equal
deleted
inserted
replaced
80 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) |
80 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) |
81 "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) (*Test_Isac_Short*) |
81 "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) (*Test_Isac_Short*) |
82 "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) (*Test_Isac_Short*) |
82 "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) (*Test_Isac_Short*) |
83 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) |
83 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) |
84 (**) |
84 (**) |
|
85 "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example" |
85 |
86 |
86 begin |
87 begin |
87 |
88 |
88 declare [[ML_print_depth = 20]] |
89 declare [[ML_print_depth = 20]] |
89 |
90 |
207 ML_file "BaseDefinitions/eval-def.sml" |
208 ML_file "BaseDefinitions/eval-def.sml" |
208 ML_file "BaseDefinitions/rewrite-order.sml" |
209 ML_file "BaseDefinitions/rewrite-order.sml" |
209 ML_file "BaseDefinitions/theoryC.sml" |
210 ML_file "BaseDefinitions/theoryC.sml" |
210 ML_file "BaseDefinitions/rule.sml" |
211 ML_file "BaseDefinitions/rule.sml" |
211 ML_file "BaseDefinitions/thmC-def.sml" |
212 ML_file "BaseDefinitions/thmC-def.sml" |
|
213 ML_file "BaseDefinitions/model-pattern.sml" |
212 ML_file "BaseDefinitions/error-fill-def.sml" |
214 ML_file "BaseDefinitions/error-fill-def.sml" |
213 ML_file "BaseDefinitions/rule-set.sml" |
215 ML_file "BaseDefinitions/rule-set.sml" |
214 ML_file "BaseDefinitions/check-unique.sml" |
216 ML_file "BaseDefinitions/check-unique.sml" |
215 (*called by Know_Store..*) |
217 (*called by Know_Store..*) |
216 ML_file "BaseDefinitions/calcelems.sml" |
218 ML_file "BaseDefinitions/calcelems.sml" |
257 ML_file "Minisubpbl/790-complete.sml" |
259 ML_file "Minisubpbl/790-complete.sml" |
258 ML_file "Minisubpbl/800-append-on-Frm.sml" |
260 ML_file "Minisubpbl/800-append-on-Frm.sml" |
259 |
261 |
260 subsection \<open>further functionality alongside batch build sequence\<close> |
262 subsection \<open>further functionality alongside batch build sequence\<close> |
261 ML_file "MathEngBasic/thmC.sml" |
263 ML_file "MathEngBasic/thmC.sml" |
|
264 ML_file "MathEngBasic/problem.sml" |
262 ML_file "MathEngBasic/rewrite.sml" |
265 ML_file "MathEngBasic/rewrite.sml" |
263 ML_file "MathEngBasic/tactic.sml" |
266 ML_file "MathEngBasic/tactic.sml" |
264 ML_file "MathEngBasic/ctree.sml" |
267 ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*) |
265 ML_file "MathEngBasic/calculation.sml" |
268 ML_file "MathEngBasic/calculation.sml" |
266 |
269 |
267 ML_file "Specify/formalise.sml" |
270 ML_file "Specify/formalise.sml" |
268 ML_file "Specify/o-model.sml" |
271 ML_file "Specify/o-model.sml" |
269 ML_file "Specify/i-model.sml" |
272 ML_file "Specify/i-model.sml" |
298 ML_file "BridgeLibisabelle/mathml.sml" (*part.*) |
301 ML_file "BridgeLibisabelle/mathml.sml" (*part.*) |
299 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml" |
302 ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml" |
300 ML_file "BridgeLibisabelle/thy-hierarchy.sml" |
303 ML_file "BridgeLibisabelle/thy-hierarchy.sml" |
301 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*) |
304 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*) |
302 ML_file "BridgeLibisabelle/interface.sml" |
305 ML_file "BridgeLibisabelle/interface.sml" |
|
306 |
303 ML_file "BridgeJEdit/parseC.sml" |
307 ML_file "BridgeJEdit/parseC.sml" |
304 ML_file "BridgeJEdit/preliminary.sml" |
308 ML_file "BridgeJEdit/preliminary.sml" |
305 ML_file "BridgeJEdit/vscode-example.sml" |
309 ML_file "BridgeJEdit/vscode-example.sml" |
306 |
310 |
307 ML_file "Knowledge/delete.sml" |
311 ML_file "Knowledge/delete.sml" |