test/Tools/isac/Test_Isac_Short.thy
changeset 60236 de0ccac9f862
parent 60230 0ca0f9363ad3
child 60239 9a28e914c469
     1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Mon Apr 19 18:05:01 2021 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Mon Apr 19 19:55:31 2021 +0200
     1.3 @@ -95,9 +95,6 @@
     1.4  
     1.5  ML \<open>open ML_System\<close>
     1.6  ML \<open>
     1.7 -\<^isac_test>\<open>
     1.8 -                      (* these vvv test, if funs are intermediately opened in structure 
     1.9 -                         in case of errors here consider ~~/xtest-to-coding.sh      *)
    1.10    open Kernel;
    1.11    open Math_Engine;
    1.12    open Test_Code;              CalcTreeTEST;
    1.13 @@ -142,7 +139,6 @@
    1.14    open Rewrite_Ord
    1.15    open UnparseC
    1.16  \<close>
    1.17 -\<close>
    1.18  
    1.19  ML \<open>
    1.20  "~~~~~ fun xxx , args:"; val () = ();