test/Tools/isac/Test_Isac.thy
changeset 59674 3da177a07c3e
parent 59659 f3f0b8d66cc8
child 59686 3ce3d089bd64
     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"