test/Tools/isac/Test_Isac_Short.thy
changeset 60223 740ebee5948b
parent 60217 1d9fee958a46
child 60230 0ca0f9363ad3
     1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Sun Apr 18 22:27:43 2021 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Sun Apr 18 23:37:59 2021 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4  
     1.5  ML \<open>open ML_System\<close>
     1.6  ML \<open>
     1.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     1.8 +\<^isac_test>\<open>
     1.9                        (* these vvv test, if funs are intermediately opened in structure 
    1.10                           in case of errors here consider ~~/xtest-to-coding.sh      *)
    1.11    open Kernel;
    1.12 @@ -141,7 +141,7 @@
    1.13    open ThmC
    1.14    open Rewrite_Ord
    1.15    open UnparseC
    1.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.17 +\<close>
    1.18  \<close>
    1.19  
    1.20  ML \<open>