1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Fri Aug 05 11:41:06 2022 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Fri Aug 05 12:30:16 2022 +0200
     1.3 @@ -50,14 +50,14 @@
     1.4       and find out, which ML_file or *.thy causes an error (might be ONLY one).
     1.5       Also backup files (#* ) recognised by jEdit cause this trouble                    *)
     1.6  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
     1.7 -(** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Thy_All"( *TODOO*)
     1.8 +(*  "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*)
     1.9  (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
    1.10  (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
    1.11  (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
    1.12  (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"
    1.13  (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units"
    1.14  (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
    1.15 -(** )"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"( *TODOO*)
    1.16 +(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
    1.17  (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
    1.18  (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
    1.19  (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo"
    1.20 @@ -228,7 +228,7 @@
    1.21    ML_file "MathEngBasic/thmC.sml"
    1.22    ML_file "MathEngBasic/rewrite.sml"
    1.23    ML_file "MathEngBasic/tactic.sml"
    1.24 -  ML_file "MathEngBasic/ctree.sml"
    1.25 +  ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*)
    1.26    ML_file "MathEngBasic/calculation.sml"
    1.27  
    1.28    ML_file "Specify/formalise.sml"
    1.29 @@ -279,10 +279,9 @@
    1.30    ML_file "Knowledge/gcd_poly_ml.sml"
    1.31    ML_file "Knowledge/rational-1.sml"
    1.32  (*ML_file "Knowledge/rational-2.sml"                                            Test_Isac_Short*)
    1.33 -ML_file "Knowledge/equation.sml"
    1.34 +  ML_file "Knowledge/equation.sml"
    1.35    ML_file "Knowledge/root.sml"
    1.36    ML_file "Knowledge/lineq.sml"
    1.37 -
    1.38  (*ML_file "Knowledge/rooteq.sml"    some complicated equations not recovered from 2002 *)
    1.39  (*ML_file "Knowledge/rateq.sml"     some complicated equations not recovered----Test_Isac_Short*)
    1.40    ML_file "Knowledge/rootrat.sml"