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 () = ();