1.1 --- a/TODO.md	Mon May 03 08:49:50 2021 +0200
     1.2 +++ b/TODO.md	Mon May 03 09:36:47 2021 +0200
     1.3 @@ -38,9 +38,6 @@
     1.4  
     1.5  * WN: simplify const names like "is'_expanded": no need to imitate the escape of mixfix syntax;
     1.6  
     1.7 -* WN: proper statement for rcancel_den ("not" is a free variable!?!!):
     1.8 -    rcancel_den:             "not(a=0) ==> a * (b / a) = b" and
     1.9 -
    1.10  * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
    1.11  
    1.12  * WN: use File.read / File.write instead of low-level TextIO operations (not portable);

     2.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon May 03 08:49:50 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Mon May 03 09:36:47 2021 +0200
     2.3 @@ -639,7 +639,7 @@
     2.4  
     2.5  	       (*----- distribute none-atoms -----*)
     2.6  	       Rule.Thm ("realpow_def_atom",ThmC.numerals_to_Free @{thm realpow_def_atom}),
     2.7 -	       (*"[| 1 < n; not(r is_atom) |]==>r  \<up>  n = r * r  \<up>  (n + -1)"*)
     2.8 +	       (*"[| 1 < n; ~ (r is_atom) |]==>r  \<up>  n = r * r  \<up>  (n + -1)"*)
     2.9  	       Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI}),
    2.10  	       (*"1  \<up>  n = 1"*)
    2.11  	       Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")

     3.1 --- a/src/Tools/isac/Knowledge/Test.thy	Mon May 03 08:49:50 2021 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Mon May 03 09:36:47 2021 +0200
     3.3 @@ -160,7 +160,7 @@
     3.4    rtwo_of_the_same_assoc:  "(x + a) + a = x + 2 * a" and
     3.5    rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" and
     3.6  
     3.7 -  rcancel_den:             "not(a=0) ==> a * (b / a) = b" and
     3.8 +  rcancel_den:             "a \<noteq> 0 ==> a * (b / a) = b" and
     3.9    rcancel_const:           "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" and
    3.10    rshift_nominator:        "(a::real) * b / c = a / c * b" and
    3.11  

     4.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Mon May 03 08:49:50 2021 +0200
     4.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Mon May 03 09:36:47 2021 +0200
     4.3 @@ -148,7 +148,7 @@
     4.4  
     4.5  UnparseC.term bdv = "x";
     4.6  UnparseC.terms asms = (* asms from rewriting are missing : vvv *)
     4.7 -  ("[\"<not> matches (?a = 0) (1 = 5 * x) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\", " ^
     4.8 +  ("[\"~ (matches (?a = 0) (1 = 5 * x)) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\", " ^
     4.9     "\"lhs (1 + -5 * x = 0) is_poly_in x\",\"lhs (1 + -5 * x = 0) has_degree_in x = 1\", " ^
    4.10     "\"1 / x = 5 is_ratequation_in x\"]");
    4.11  (*