diff -r 638d02a9a96a -r e6e7a9b9ced7 test/Tools/isac/Test_Isac_Short.thy --- a/test/Tools/isac/Test_Isac_Short.thy Tue Jun 01 15:41:23 2021 +0200 +++ b/test/Tools/isac/Test_Isac_Short.thy Sat Jul 03 16:21:07 2021 +0200 @@ -230,15 +230,6 @@ subsection \further functionality alongside batch build sequence\ ML_file "MathEngBasic/thmC.sml" ML_file "MathEngBasic/rewrite.sml" -ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML \ -\ ML_file "MathEngBasic/tactic.sml" ML_file "MathEngBasic/ctree.sml" ML_file "MathEngBasic/calculation.sml" @@ -293,13 +284,14 @@ ML_file "Knowledge/poly.sml" ML_file "Knowledge/gcd_poly_ml.sml" ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*) -(*ML_file "Knowledge/rational.sml" Test_Isac_Short*) + ML_file "Knowledge/rational.sml" (*Test_Isac_Short*) ML_file "Knowledge/equation.sml" ML_file "Knowledge/root.sml" ML_file "Knowledge/lineq.sml" + (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *) (*ML_file "Knowledge/rateq.sml" some complicated equations not recovered----Test_Isac_Short*) - ML_file "Knowledge/rootrat.sml" + ML_file "Knowledge/r/ootrat.sml" ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*) ML_file "Knowledge/polyeq-1.sml"