equal
deleted
inserted
replaced
2 imports "Isac.Build_Isac" |
2 imports "Isac.Build_Isac" |
3 begin |
3 begin |
4 |
4 |
5 ML \<open>open ML_System\<close> |
5 ML \<open>open ML_System\<close> |
6 ML \<open> |
6 ML \<open> |
7 \<^isac_test>\<open> |
|
8 (* these vvv test, if funs are intermediately opened in structure |
|
9 in case of errors here consider ~~/xtest-to-coding.sh *) |
|
10 open Kernel; |
7 open Kernel; |
11 open Math_Engine; |
8 open Math_Engine; |
12 open Test_Code; CalcTreeTEST; |
9 open Test_Code; CalcTreeTEST; |
13 open LItool; arguments_from_model; |
10 open LItool; arguments_from_model; |
14 open Sub_Problem; |
11 open Sub_Problem; |
49 open ThmC_Def |
46 open ThmC_Def |
50 open ThmC |
47 open ThmC |
51 open Rewrite_Ord |
48 open Rewrite_Ord |
52 open UnparseC |
49 open UnparseC |
53 \<close> |
50 \<close> |
54 \<close> |
|
55 ML_file "BridgeJEdit/parseC.sml" |
51 ML_file "BridgeJEdit/parseC.sml" |
56 |
52 |
57 section \<open>code for copy & paste ===============================================================\<close> |
53 section \<open>code for copy & paste ===============================================================\<close> |
58 ML \<open> |
54 ML \<open> |
59 "~~~~~ fun xxx , args:"; val () = (); |
55 "~~~~~ fun xxx , args:"; val () = (); |