equal
deleted
inserted
replaced
129 open Celem; e_pbt; |
129 open Celem; e_pbt; |
130 open Rule; |
130 open Rule; |
131 open Rule_Set |
131 open Rule_Set |
132 open Exec_Def |
132 open Exec_Def |
133 open ThyC |
133 open ThyC |
|
134 open ThmC_Def |
134 open ThmC |
135 open ThmC |
135 open Rewrite_Ord |
136 open Rewrite_Ord |
136 open UnparseC |
137 open UnparseC |
137 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
138 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
138 \<close> |
139 \<close> |
181 ML_file "CalcElements/rule-def.sml" |
182 ML_file "CalcElements/rule-def.sml" |
182 ML_file "CalcElements/exec-def.sml" |
183 ML_file "CalcElements/exec-def.sml" |
183 ML_file "CalcElements/rewrite-order.sml" |
184 ML_file "CalcElements/rewrite-order.sml" |
184 ML_file "CalcElements/theoryC.sml" |
185 ML_file "CalcElements/theoryC.sml" |
185 ML_file "CalcElements/rule.sml" |
186 ML_file "CalcElements/rule.sml" |
186 ML_file "CalcElements/thmC.sml" |
187 ML_file "CalcElements/thmC-def.sml" |
187 ML_file "CalcElements/error-fill-def.sml" |
188 ML_file "CalcElements/error-fill-def.sml" |
188 ML_file "CalcElements/rule-set.sml" |
189 ML_file "CalcElements/rule-set.sml" |
189 ML_file "CalcElements/calcelems.sml" |
190 ML_file "CalcElements/calcelems.sml" |
190 ML_file "CalcElements/termC.sml" |
191 ML_file "CalcElements/termC.sml" |
191 ML_file "CalcElements/contextC.sml" |
192 ML_file "CalcElements/contextC.sml" |
198 ML_file "ProgLang/prog_expr.sml" |
199 ML_file "ProgLang/prog_expr.sml" |
199 ML_file "ProgLang/program.sml" |
200 ML_file "ProgLang/program.sml" |
200 ML_file "ProgLang/prog_tac.sml" |
201 ML_file "ProgLang/prog_tac.sml" |
201 ML_file "ProgLang/tactical.sml" |
202 ML_file "ProgLang/tactical.sml" |
202 ML_file "ProgLang/auto_prog.sml" |
203 ML_file "ProgLang/auto_prog.sml" |
203 ML_file "ProgLang/rewrite.sml" |
|
204 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- |
204 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- |
205 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) |
205 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) |
206 |
206 |
207 subsection \<open>basic functionality on simple example first\<close> |
207 subsection \<open>basic functionality on simple example first\<close> |
208 ML_file "Minisubpbl/000-comments.sml" |
208 ML_file "Minisubpbl/000-comments.sml" |
226 ML_file "Minisubpbl/790-complete-NEXT_STEP.sml" |
226 ML_file "Minisubpbl/790-complete-NEXT_STEP.sml" |
227 ML_file "Minisubpbl/790-complete.sml" |
227 ML_file "Minisubpbl/790-complete.sml" |
228 ML_file "Minisubpbl/800-append-on-Frm.sml" |
228 ML_file "Minisubpbl/800-append-on-Frm.sml" |
229 |
229 |
230 subsection \<open>further functionality alongside batch build sequence\<close> |
230 subsection \<open>further functionality alongside batch build sequence\<close> |
|
231 ML_file "MathEngBasic/thmC.sml" |
|
232 ML_file "MathEngBasic/rewrite.sml" |
231 ML_file "MathEngBasic/model.sml" |
233 ML_file "MathEngBasic/model.sml" |
232 ML_file "MathEngBasic/mstools.sml" |
234 ML_file "MathEngBasic/mstools.sml" |
233 ML_file "MathEngBasic/specification-elems.sml" |
235 ML_file "MathEngBasic/specification-elems.sml" |
234 ML_file "MathEngBasic/tactic.sml" |
236 ML_file "MathEngBasic/tactic.sml" |
235 ML_file "MathEngBasic/ctree.sml" |
237 ML_file "MathEngBasic/ctree.sml" |