1.1 --- a/TODO.md	Tue Apr 20 23:20:45 2021 +0200
     1.2 +++ b/TODO.md	Wed Apr 21 10:09:14 2021 +0200
     1.3 @@ -5,12 +5,6 @@
     1.4  
     1.5  * WN: check remaining "for tests only" wrt. \<^isac_test>CARTOUCHE;
     1.6  
     1.7 -* WN: eliminate odd notation term tricks: replace "^^^" e.g. by "\<up>"
     1.8 -  based on "_ powr _" for type real;
     1.9 -
    1.10 -    abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real"  (infixr "\<up>" 80)
    1.11 -      where "x \<up> a \<equiv> x powr a"
    1.12 -
    1.13  * WN: purge BridgeLibisabelle: eliminate unused code;
    1.14  
    1.15  
    1.16 @@ -45,6 +39,8 @@
    1.17      - sometimes this requires to use more specific types / type classes;
    1.18      - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
    1.19      - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
    1.20 +    - abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real"  (infixr "\<up>" 80)
    1.21 +      where "x \<up> a \<equiv> x powr a"
    1.22  
    1.23  * WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation
    1.24      - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");

     2.1 --- a/test/Tools/isac/Knowledge/poly.sml	Tue Apr 20 23:20:45 2021 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/poly.sml	Wed Apr 21 10:09:14 2021 +0200
     2.3 @@ -456,7 +456,7 @@
     2.4  "-----SPB Schalk I p.64 No.296c ---";
     2.5  val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
     2.6  val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
     2.7 -if (UnparseC.term t) = "-27 * x \<up> 3 + -108 * x \<up> 2 * y + -144 * x * y \<up> 2 + -64 * y \<up> 3"
     2.8 +if (UnparseC.term t) = "-27 * x \<up> 3 + -108 * x \<up> 2 * y + -144 * x * y \<up> 2 +\n-64 * y \<up> 3"
     2.9  then () else error "poly.sml: diff.behav. in make_polynomial 11";
    2.10  
    2.11  "-----SPB Schalk I p.62 No.242c ---";
    2.12 @@ -635,13 +635,11 @@
    2.13  
    2.14  (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Empty_Tac: ERROR DETECTED Feb.2020*)
    2.15  
    2.16 -(*+*)if f2str f = "17 + 15 * x \<up> 2 + -48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 + -8 * x \<up> 9"
    2.17 -(*+*)then () else error "";
    2.18 +(*+*)if f2str f = "17 + 15 * x \<up> 2 + -48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n-8 * x \<up> 9"
    2.19 +(*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b -1";
    2.20  
    2.21  (*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 LItool.find_next_step without result*)
    2.22  
    2.23 -(*+*)if f2str f = "17 + 15 * x \<up> 2 + -48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 + -8 * x \<up> 9"
    2.24 -(*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b";
    2.25  
    2.26  
    2.27  "-------- interSteps for Schalk 299a --------------------";

     3.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Tue Apr 20 23:20:45 2021 +0200
     3.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Wed Apr 21 10:09:14 2021 +0200
     3.3 @@ -277,7 +277,7 @@
     3.4    ML_file "Knowledge/delete.sml"
     3.5    ML_file "Knowledge/descript.sml"
     3.6    ML_file "Knowledge/simplify.sml"
     3.7 -(*ML_file "Knowledge/poly.sml" ONLY ERROR BY REPLACING ^^^ \<rightarrow>  \<up> *)
     3.8 +  ML_file "Knowledge/poly.sml"
     3.9    ML_file "Knowledge/gcd_poly_ml.sml"
    3.10    ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
    3.11  (*ML_file "Knowledge/rational.sml"                                              Test_Isac_Short*)