1.1 --- a/test/Tools/isac/Test_Isac.thy Fri Oct 25 16:07:15 2019 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Sat Oct 26 13:03:16 2019 +0200
1.3 @@ -131,8 +131,12 @@
1.4 \<close>
1.5
1.6 ML \<open>
1.7 -"~~~~~ fun xxx, args:"; val () = ();
1.8 -\<close> ML \<open>
1.9 +"~~~~~ fun xxx , args:"; val () = ();
1.10 +"~~~~~ and xxx , args:"; val () = ();
1.11 +"~~~~~ from xxx to yyy return val:"; val () = ();
1.12 +(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);
1.13 +"xx"
1.14 +^ "xxx" (*+*)
1.15 \<close> ML \<open>
1.16 \<close>
1.17
1.18 @@ -192,10 +196,11 @@
1.19 ML_file "Minisubpbl/799-complete.sml"
1.20
1.21 subsection \<open>further functionality alongside batch build sequence\<close>
1.22 - ML_file "Specify/model.sml"
1.23 - ML_file "Specify/mstools.sml"
1.24 - ML_file "Specify/specification-elems.sml"
1.25 - ML_file "Specify/ctree.sml" (*!...!see(25)*)
1.26 + ML_file "MathEngBasic/model.sml"
1.27 + ML_file "MathEngBasic/mstools.sml"
1.28 + ML_file "MathEngBasic/specification-elems.sml"
1.29 + ML_file "MathEngBasic/ctree.sml" (*!...!see(25)*)
1.30 +
1.31 ML_file "Specify/ptyps.sml" (* requires setup from ptyps.thy *)
1.32 ML \<open>(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\<close>
1.33 ML_file "Specify/generate.sml"