equal
deleted
inserted
replaced
23 "../../Pure/Isar/Test_Parse_Term" |
23 "../../Pure/Isar/Test_Parse_Term" |
24 |
24 |
25 uses |
25 uses |
26 ( "library.sml") |
26 ( "library.sml") |
27 ( "calcelems.sml") |
27 ( "calcelems.sml") |
28 ("ProgLang/termC.sml") |
28 ("ProgLang/termC.sml") |
29 ("ProgLang/calculate.sml") |
29 ("ProgLang/calculate.sml") |
30 ("ProgLang/rewrite.sml") |
30 ("ProgLang/rewrite.sml") |
31 (*("ProgLang/listg.sml")*) |
31 ("ProgLang/listg.sml") |
32 ("ProgLang/scrtools.sml") |
32 ("ProgLang/scrtools.sml") |
33 ("ProgLang/tools.sml") |
33 ("ProgLang/tools.sml") |
34 |
34 |
35 ("Minisubpbl/000-comments.sml") |
35 ("Minisubpbl/000-comments.sml") |
36 ("Minisubpbl/100-init-rootpbl.sml") |
36 ("Minisubpbl/100-init-rootpbl.sml") |
76 ("Knowledge/root.sml") |
76 ("Knowledge/root.sml") |
77 ("Knowledge/lineq.sml") |
77 ("Knowledge/lineq.sml") |
78 ("Knowledge/rooteq.sml") |
78 ("Knowledge/rooteq.sml") |
79 ("Knowledge/rateq.sml") |
79 ("Knowledge/rateq.sml") |
80 ("Knowledge/rootrateq.sml") |
80 ("Knowledge/rootrateq.sml") |
81 (*("Knowledge/polyeq.sml")*) |
81 ("Knowledge/polyeq.sml") |
82 ("Knowledge/calculus.sml") |
82 ("Knowledge/calculus.sml") |
83 ("Knowledge/trig.sml") |
83 ("Knowledge/trig.sml") |
84 ("Knowledge/logexp.sml") |
84 ("Knowledge/logexp.sml") |
85 ("Knowledge/diff.sml") |
85 ("Knowledge/diff.sml") |
86 ("Knowledge/integrate.sml") |
86 ("Knowledge/integrate.sml") |
97 begin |
97 begin |
98 |
98 |
99 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*} |
99 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*} |
100 use "library.sml" |
100 use "library.sml" |
101 use "calcelems.sml" |
101 use "calcelems.sml" |
102 use "ProgLang/termC.sml |
102 use "ProgLang/termC.sml" |
103 use "ProgLang/calculate.sml" (*part.*) |
103 use "ProgLang/calculate.sml" (*part.*) |
104 use "ProgLang/rewrite.sml" (*part.*) |
104 use "ProgLang/rewrite.sml" (*part.*) |
105 (*use "ProgLang/listg.sml" 2002*) |
105 (*use "ProgLang/listC.sml" 2002*) |
106 use "ProgLang/scrtools.sml" (*complete*) |
106 use "ProgLang/scrtools.sml" (*complete*) |
107 use "ProgLang/tools.sml" (*complete*) |
107 use "ProgLang/tools.sml" (*complete*) |
108 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*} |
108 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*} |
109 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*} |
109 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*} |
110 use "Minisubpbl/000-comments.sml" |
110 use "Minisubpbl/000-comments.sml" |
117 use "Minisubpbl/500-met-sub-to-root.sml" |
117 use "Minisubpbl/500-met-sub-to-root.sml" |
118 use "Minisubpbl/530-error-Check_Elementwise.sml" |
118 use "Minisubpbl/530-error-Check_Elementwise.sml" |
119 use "Minisubpbl/600-postcond.sml" |
119 use "Minisubpbl/600-postcond.sml" |
120 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*} |
120 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*} |
121 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*} |
121 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*} |
122 use "Interpret/mstools.sml" (*new 2010*) |
122 use "Interpret/mstools.sml" |
123 use "Interpret/ctree.sml" (*!...!see(25)*) |
123 use "Interpret/ctree.sml" (*!...!see(25)*) |
124 use "Interpret/ptyps.sml" (* *) |
124 use "Interpret/ptyps.sml" (* *) |
125 (*use "Interpret/generate.sml" new 2011*) |
125 (*use "Interpret/generate.sml" new 2011*) |
126 use "Interpret/calchead.sml" (*part.*) |
126 use "Interpret/calchead.sml" (*part.*) |
127 use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*) |
127 use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*) |