1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Mon Aug 02 11:38:40 2021 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Mon Aug 02 15:25:49 2021 +0200
     1.3 @@ -190,7 +190,7 @@
     1.4    ML_file "BaseDefinitions/calcelems.sml"
     1.5    ML_file "BaseDefinitions/termC.sml"
     1.6    ML_file "BaseDefinitions/substitution.sml"
     1.7 -  ML_file "BaseDefinitions/contextC.sml"        (*TOODOO make_ratpoly: "- 6 * x"  \<longrightarrow>  "- (6 * x)"*)
     1.8 +  ML_file "BaseDefinitions/contextC.sml"
     1.9    ML_file "BaseDefinitions/environment.sml"
    1.10  (** )ML_file "BaseDefinitions/kestore.sml" ( * setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
    1.11  (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
    1.12 @@ -234,7 +234,7 @@
    1.13    ML_file "MathEngBasic/thmC.sml"
    1.14    ML_file "MathEngBasic/rewrite.sml"
    1.15    ML_file "MathEngBasic/tactic.sml"
    1.16 -(** )ML_file "MathEngBasic/ctree.sml"            ( ** )loops with eliminate ThmC.numerals_to_Free*)
    1.17 +  ML_file "MathEngBasic/ctree.sml"
    1.18    ML_file "MathEngBasic/calculation.sml"
    1.19  
    1.20    ML_file "Specify/formalise.sml"
    1.21 @@ -272,8 +272,7 @@
    1.22    ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
    1.23    ML_file "BridgeLibisabelle/thy-hierarchy.sml"
    1.24    ML_file "BridgeLibisabelle/interface-xml.sml"     (*TODO after 2009- 2*)
    1.25 -(** )ML_file "BridgeLibisabelle/interface.sml"( *loops with eliminate ThmC.numerals_to_Free
    1.26 -                                                 but is deprecated after ^^^^^^^^^^^^^^^( **)
    1.27 +  ML_file "BridgeLibisabelle/interface.sml"
    1.28    ML_file "BridgeJEdit/parseC.sml"
    1.29    ML_file "BridgeJEdit/preliminary.sml"
    1.30  
    1.31 @@ -287,15 +286,15 @@
    1.32    ML_file "Knowledge/rational-1.sml"
    1.33  (*ML_file "Knowledge/rational-2.sml"                                            Test_Isac_Short*)
    1.34    ML_file "Knowledge/equation.sml"
    1.35 -(*ML_file "Knowledge/root.sml"                                    see TOODOO.1*)
    1.36 +(*ML_file "Knowledge/root.sml"                                                        see TOODOO.1*)
    1.37    ML_file "Knowledge/lineq.sml"
    1.38  
    1.39  (*ML_file "Knowledge/rooteq.sml"    some complicated equations not recovered from 2002 *)
    1.40  (*ML_file "Knowledge/rateq.sml"     some complicated equations not recovered----Test_Isac_Short*)
    1.41 -(*ML_file "Knowledge/rootrat.sml"                                    error inherited from root.sml*)
    1.42 +(*ML_file "Knowledge/rootrat.sml"                           TOODOO.1 error inherited from root.sml*)
    1.43    ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
    1.44  (*ML_file "Knowledge/partial_fractions.sml"  hangs with ML_system_64 = "true"---Test_Isac_Short*)
    1.45 -(*ML_file "Knowledge/polyeq-1.sml"                error inherited from root.sml | in Test_Some.thy*)
    1.46 +(*ML_file "Knowledge/polyeq-1.sml"                          TOODOO.1 error inherited from root.sml*)
    1.47  (*ML_file "Knowledge/polyeq-2.sml"                                              Test_Isac_Short*)
    1.48  (*ML_file "Knowledge/rlang.sml"     much to clean up, similar tests in other files     *)
    1.49    ML_file "Knowledge/calculus.sml"