equal
deleted
inserted
replaced
20 (*imports Complex_Main*) |
20 (*imports Complex_Main*) |
21 imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*) |
21 imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*) |
22 begin |
22 begin |
23 |
23 |
24 ML {* Toplevel.debug := true; *} |
24 ML {* Toplevel.debug := true; *} |
25 |
|
26 use "library.sml" |
25 use "library.sml" |
27 use "calcelems.sml" |
26 use "calcelems.sml" |
28 ML {* check_guhs_unique := true *} |
27 ML {* check_guhs_unique := true *} |
29 |
28 |
30 use "Scripts/term_G.sml" |
29 use "Scripts/term_G.sml" |
33 use_thy"Scripts/Script" |
32 use_thy"Scripts/Script" |
34 use "Scripts/scrtools.sml" |
33 use "Scripts/scrtools.sml" |
35 |
34 |
36 use "ME/mstools.sml" |
35 use "ME/mstools.sml" |
37 use "ME/ctree.sml" |
36 use "ME/ctree.sml" |
|
37 use "ME/ptyps.sml" |
38 |
38 |
39 |
39 |
40 ML {* |
40 ML {* |
41 member; |
41 member; |
42 @{term 111}; |
42 @{term 111}; |
43 *} |
43 *} |
44 |
44 |
45 |
45 |
46 (* |
46 (* |
47 use "ME/ptyps.sml" |
|
48 use "ME/generate.sml" |
47 use "ME/generate.sml" |
49 use "ME/calchead.sml" |
48 use "ME/calchead.sml" |
50 use "ME/appl.sml" |
49 use "ME/appl.sml" |
51 use "ME/rewtools.sml" |
50 use "ME/rewtools.sml" |
52 use "ME/script.sml" |
51 use "ME/script.sml" |