1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Mon Apr 19 20:44:18 2021 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Tue Apr 20 16:58:44 2021 +0200
     1.3 @@ -184,18 +184,6 @@
     1.4  (*called by Know_Store..*)
     1.5    ML_file "BaseDefinitions/calcelems.sml"
     1.6    ML_file "BaseDefinitions/termC.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> ML \<open>
    1.16 -\<close> ML \<open>
    1.17 -\<close> ML \<open>
    1.18 -\<close>
    1.19    ML_file "BaseDefinitions/substitution.sml"
    1.20    ML_file "BaseDefinitions/contextC.sml"
    1.21    ML_file "BaseDefinitions/environment.sml"
    1.22 @@ -289,7 +277,7 @@
    1.23    ML_file "Knowledge/delete.sml"
    1.24    ML_file "Knowledge/descript.sml"
    1.25    ML_file "Knowledge/simplify.sml"
    1.26 -  ML_file "Knowledge/poly.sml"
    1.27 +(*ML_file "Knowledge/poly.sml" ONLY ERROR BY REPLACING ^^^ \<rightarrow>  \<up> *)
    1.28    ML_file "Knowledge/gcd_poly_ml.sml"
    1.29    ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
    1.30  (*ML_file "Knowledge/rational.sml"                                              Test_Isac_Short*)
    1.31 @@ -578,7 +566,7 @@
    1.32    --------------------------------------------------------------------------------
    1.33    WN120317.TODO changeset 977788dfed26 dropped rateq:
    1.34    # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
    1.35 -  # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:    
    1.36 +  # test --- solve (1/x = 5, x) by me --- and --- x / (x  \<up>  2 - 6 * x + 9) - ...:    
    1.37      investigation Check_elementwise stopped due to too much effort finding out,
    1.38      why Check_elementwise worked in 2002 in spite of the error.
    1.39    --------------------------------------------------------------------------------
    1.40 @@ -596,7 +584,7 @@
    1.41    FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
    1.42    # mark twice thms (in isac + (later) in Isabelle) in Isac.thy
    1.43    --------------------------------------------------------------------------------
    1.44 -  WN120320.TODO rlsthmsNOTisac: replace twice thms ^
    1.45 +  WN120320.TODO rlsthmsNOTisac: replace twice thms  \<up> 
    1.46    --------------------------------------------------------------------------------
    1.47    WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
    1.48    --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.