1.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue Jul 20 14:37:56 2021 +0200
1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Jul 27 11:21:14 2021 +0200
1.3 @@ -228,11 +228,11 @@
1.4 ML_file "Minisubpbl/710-interSteps-short.sml"
1.5 ML_file "Minisubpbl/790-complete-NEXT_STEP.sml"
1.6 ML_file "Minisubpbl/790-complete.sml"
1.7 - ML_file "Minisubpbl/800-append-on-Frm.sml"(*STARTbroken with "reduce the number of TermC.parse*"*)
1.8 + ML_file "Minisubpbl/800-append-on-Frm.sml"
1.9
1.10 subsection \<open>further functionality alongside batch build sequence\<close>
1.11 ML_file "MathEngBasic/thmC.sml"
1.12 - ML_file "MathEngBasic/rewrite.sml"
1.13 + ML_file "MathEngBasic/rewrite.sml"
1.14 ML_file "MathEngBasic/tactic.sml"
1.15 (** )ML_file "MathEngBasic/ctree.sml" ( ** )loops with eliminate ThmC.numerals_to_Free*)
1.16 ML_file "MathEngBasic/calculation.sml"
1.17 @@ -254,16 +254,16 @@
1.18
1.19 ML_file "Interpret/istate.sml"
1.20 ML_file "Interpret/sub-problem.sml"
1.21 - ML_file "Interpret/error-pattern.sml" (*broken with "reduce the number of TermC.parse*"*)
1.22 + ML_file "Interpret/error-pattern.sml"
1.23 ML_file "Interpret/li-tool.sml"
1.24 - ML_file "Interpret/lucas-interpreter.sml" (*broken with "reduce the number of TermC.parse*"*)
1.25 + ML_file "Interpret/lucas-interpreter.sml"
1.26 ML_file "Interpret/step-solve.sml"
1.27
1.28 ML_file "MathEngine/me-misc.sml"
1.29 ML_file "MathEngine/fetch-tactics.sml"
1.30 ML_file "MathEngine/solve.sml"
1.31 ML_file "MathEngine/step.sml"
1.32 - ML_file "MathEngine/mathengine-stateless.sml" (*broken with "reduce the number of TermC.parse*"*)
1.33 + ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*)
1.34 ML_file "MathEngine/messages.sml"
1.35 ML_file "MathEngine/states.sml"
1.36
1.37 @@ -280,7 +280,7 @@
1.38 ML_file "Knowledge/delete.sml"
1.39 ML_file "Knowledge/descript.sml"
1.40 ML_file "Knowledge/simplify.sml"
1.41 -(* ML_file "Knowledge/poly-1.sml" broken with "reduce the number of TermC.parse*"*)
1.42 + ML_file "Knowledge/poly-1.sml"
1.43 (*ML_file "Knowledge/poly-2.sml" Test_Isac_Short*)
1.44 ML_file "Knowledge/gcd_poly_ml.sml"
1.45 ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
1.46 @@ -322,21 +322,7 @@
1.47 ML_file "Test_Code/test-code.sml"
1.48
1.49 section \<open>further tests additional to src/.. files\<close>
1.50 -(*ML_file "BridgeLibisabelle/use-cases.sml" broken with "reduce the number of TermC.parse*"*)
1.51 -ML \<open>
1.52 -\<close> ML \<open>
1.53 -(*TOODOO broken with "reduce the number of TermC.parse---------------------------------------\\*"
1.54 - TOODOObroken with "reduce the number of TermC.parse*"--------------------------------------//*)
1.55 -\<close> ML \<open>
1.56 -\<close> ML \<open>
1.57 -\<close> ML \<open>
1.58 -\<close> ML \<open>
1.59 -\<close> ML \<open>
1.60 -\<close> ML \<open>
1.61 -\<close> ML \<open>
1.62 -\<close> ML \<open>
1.63 -\<close> ML \<open>
1.64 -\<close>
1.65 + ML_file "BridgeLibisabelle/use-cases.sml"
1.66
1.67 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.68 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>