48 imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*) |
48 imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*) |
49 (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one |
49 (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one |
50 and find out, which ML_file or *.thy causes an error (might be ONLY one). |
50 and find out, which ML_file or *.thy causes an error (might be ONLY one). |
51 Also backup files (#* ) recognised by jEdit cause this trouble *) |
51 Also backup files (#* ) recognised by jEdit cause this trouble *) |
52 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) |
52 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) |
53 (** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Thy_All"( *TODOO*) |
53 (* "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*) |
54 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter" |
54 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter" |
55 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt" |
55 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt" |
56 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test" |
56 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test" |
57 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt" |
57 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt" |
58 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units" |
58 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units" |
59 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics" |
59 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics" |
60 (** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"( *TODOO*) |
60 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting" |
61 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine" |
61 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine" |
62 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test" |
62 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test" |
63 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo" |
63 (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo" |
64 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform" |
64 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform" |
65 ADDTESTS/------------------------------------------- see end of tests *) |
65 ADDTESTS/------------------------------------------- see end of tests *) |
226 |
226 |
227 subsection \<open>further functionality alongside batch build sequence\<close> |
227 subsection \<open>further functionality alongside batch build sequence\<close> |
228 ML_file "MathEngBasic/thmC.sml" |
228 ML_file "MathEngBasic/thmC.sml" |
229 ML_file "MathEngBasic/rewrite.sml" |
229 ML_file "MathEngBasic/rewrite.sml" |
230 ML_file "MathEngBasic/tactic.sml" |
230 ML_file "MathEngBasic/tactic.sml" |
231 ML_file "MathEngBasic/ctree.sml" |
231 ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*) |
232 ML_file "MathEngBasic/calculation.sml" |
232 ML_file "MathEngBasic/calculation.sml" |
233 |
233 |
234 ML_file "Specify/formalise.sml" |
234 ML_file "Specify/formalise.sml" |
235 ML_file "Specify/o-model.sml" |
235 ML_file "Specify/o-model.sml" |
236 ML_file "Specify/i-model.sml" |
236 ML_file "Specify/i-model.sml" |
277 ML_file "Knowledge/poly-1.sml" |
277 ML_file "Knowledge/poly-1.sml" |
278 (*ML_file "Knowledge/poly-2.sml" Test_Isac_Short*) |
278 (*ML_file "Knowledge/poly-2.sml" Test_Isac_Short*) |
279 ML_file "Knowledge/gcd_poly_ml.sml" |
279 ML_file "Knowledge/gcd_poly_ml.sml" |
280 ML_file "Knowledge/rational-1.sml" |
280 ML_file "Knowledge/rational-1.sml" |
281 (*ML_file "Knowledge/rational-2.sml" Test_Isac_Short*) |
281 (*ML_file "Knowledge/rational-2.sml" Test_Isac_Short*) |
282 ML_file "Knowledge/equation.sml" |
282 ML_file "Knowledge/equation.sml" |
283 ML_file "Knowledge/root.sml" |
283 ML_file "Knowledge/root.sml" |
284 ML_file "Knowledge/lineq.sml" |
284 ML_file "Knowledge/lineq.sml" |
285 |
|
286 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *) |
285 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *) |
287 (*ML_file "Knowledge/rateq.sml" some complicated equations not recovered----Test_Isac_Short*) |
286 (*ML_file "Knowledge/rateq.sml" some complicated equations not recovered----Test_Isac_Short*) |
288 ML_file "Knowledge/rootrat.sml" |
287 ML_file "Knowledge/rootrat.sml" |
289 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) |
288 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) |
290 (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*) |
289 (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*) |