equal
deleted
inserted
replaced
1 theory Test_Some imports Isac |
1 theory Test_Some imports Isac |
2 begin |
2 begin |
3 ML_file "Knowledge/diff.sml" |
3 ML_file "Interpret/mstools.sml" |
4 |
4 |
5 section {* code for copy & paste ===============================================================*} |
5 section {* code for copy & paste ===============================================================*} |
6 ML {* |
6 ML {* |
7 "~~~~~ fun , args:"; val () = (); |
7 "~~~~~ fun , args:"; val () = (); |
8 "~~~~~ and , args:"; val () = (); |
8 "~~~~~ and , args:"; val () = (); |
24 ============ inhibit exn WN130909 TODO ========================================================*) |
24 ============ inhibit exn WN130909 TODO ========================================================*) |
25 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
25 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
26 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*) |
26 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*) |
27 *} |
27 *} |
28 |
28 |
|
29 thm mult_commute |
|
30 |
29 section {* ===================================================================================*} |
31 section {* ===================================================================================*} |
30 ML {* |
32 ML {* |
31 *} ML {* |
33 *} ML {* |
32 *} ML {* |
34 *} ML {* |
33 *} ML {* |
35 *} ML {* |
34 *} |
36 *} |
35 |
37 |
36 section {* ===================================================================================*} |
38 section {* ===================================================================================*} |
37 ML {* |
39 ML {* |
38 *} ML {* |
40 *} ML {* |
39 *} ML {* |
41 *} ML {* |