1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Tue Jun 01 15:41:23 2021 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Sat Jul 03 16:21:07 2021 +0200
     1.3 @@ -230,15 +230,6 @@
     1.4  subsection \<open>further functionality alongside batch build sequence\<close>
     1.5    ML_file "MathEngBasic/thmC.sml"
     1.6    ML_file "MathEngBasic/rewrite.sml"
     1.7 -ML \<open>
     1.8 -\<close> ML \<open>
     1.9 -\<close> ML \<open>
    1.10 -\<close> ML \<open>
    1.11 -\<close> ML \<open>
    1.12 -\<close> ML \<open>
    1.13 -\<close> ML \<open>
    1.14 -\<close> ML \<open>
    1.15 -\<close>
    1.16    ML_file "MathEngBasic/tactic.sml"
    1.17    ML_file "MathEngBasic/ctree.sml"
    1.18    ML_file "MathEngBasic/calculation.sml"
    1.19 @@ -293,13 +284,14 @@
    1.20    ML_file "Knowledge/poly.sml"
    1.21    ML_file "Knowledge/gcd_poly_ml.sml"
    1.22    ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
    1.23 -(*ML_file "Knowledge/rational.sml"                                              Test_Isac_Short*)
    1.24 +  ML_file "Knowledge/rational.sml"                                            (*Test_Isac_Short*)
    1.25    ML_file "Knowledge/equation.sml"
    1.26    ML_file "Knowledge/root.sml"
    1.27    ML_file "Knowledge/lineq.sml"
    1.28 +
    1.29  (*ML_file "Knowledge/rooteq.sml"    some complicated equations not recovered from 2002 *)
    1.30  (*ML_file "Knowledge/rateq.sml"     some complicated equations not recovered----Test_Isac_Short*)
    1.31 -  ML_file "Knowledge/rootrat.sml"
    1.32 +  ML_file "Knowledge/r/ootrat.sml"
    1.33    ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
    1.34  (*ML_file "Knowledge/partial_fractions.sml"  hangs with ML_system_64 = "true"---Test_Isac_Short*)
    1.35    ML_file "Knowledge/polyeq-1.sml"