# HG changeset patch
# User wneuper <walther.neuper@jku.at>
# Date 1620027407 -7200
# Node ID e898eeaab29aa1435d5ba45443d9776255bdd00b
# Parent  98ee674d18d314a29c8e89a1b6c7b00b07384765
eliminate old "not" (now a free variable) in terms

diff -r 98ee674d18d3 -r e898eeaab29a TODO.md
--- a/TODO.md	Mon May 03 08:49:50 2021 +0200
+++ b/TODO.md	Mon May 03 09:36:47 2021 +0200
@@ -38,9 +38,6 @@
 
 * WN: simplify const names like "is'_expanded": no need to imitate the escape of mixfix syntax;
 
-* WN: proper statement for rcancel_den ("not" is a free variable!?!!):
-    rcancel_den:             "not(a=0) ==> a * (b / a) = b" and
-
 * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
 
 * WN: use File.read / File.write instead of low-level TextIO operations (not portable);
diff -r 98ee674d18d3 -r e898eeaab29a src/Tools/isac/Knowledge/Rational.thy
--- a/src/Tools/isac/Knowledge/Rational.thy	Mon May 03 08:49:50 2021 +0200
+++ b/src/Tools/isac/Knowledge/Rational.thy	Mon May 03 09:36:47 2021 +0200
@@ -639,7 +639,7 @@
 
 	       (*----- distribute none-atoms -----*)
 	       Rule.Thm ("realpow_def_atom",ThmC.numerals_to_Free @{thm realpow_def_atom}),
-	       (*"[| 1 < n; not(r is_atom) |]==>r  \<up>  n = r * r  \<up>  (n + -1)"*)
+	       (*"[| 1 < n; ~ (r is_atom) |]==>r  \<up>  n = r * r  \<up>  (n + -1)"*)
 	       Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI}),
 	       (*"1  \<up>  n = 1"*)
 	       Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
diff -r 98ee674d18d3 -r e898eeaab29a src/Tools/isac/Knowledge/Test.thy
--- a/src/Tools/isac/Knowledge/Test.thy	Mon May 03 08:49:50 2021 +0200
+++ b/src/Tools/isac/Knowledge/Test.thy	Mon May 03 09:36:47 2021 +0200
@@ -160,7 +160,7 @@
   rtwo_of_the_same_assoc:  "(x + a) + a = x + 2 * a" and
   rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" and
 
-  rcancel_den:             "not(a=0) ==> a * (b / a) = b" and
+  rcancel_den:             "a \<noteq> 0 ==> a * (b / a) = b" and
   rcancel_const:           "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" and
   rshift_nominator:        "(a::real) * b / c = a / c * b" and
 
diff -r 98ee674d18d3 -r e898eeaab29a test/Tools/isac/Knowledge/rateq.sml
--- a/test/Tools/isac/Knowledge/rateq.sml	Mon May 03 08:49:50 2021 +0200
+++ b/test/Tools/isac/Knowledge/rateq.sml	Mon May 03 09:36:47 2021 +0200
@@ -148,7 +148,7 @@
 
 UnparseC.term bdv = "x";
 UnparseC.terms asms = (* asms from rewriting are missing : vvv *)
-  ("[\"<not> matches (?a = 0) (1 = 5 * x) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\", " ^
+  ("[\"~ (matches (?a = 0) (1 = 5 * x)) | ~ lhs (1 = 5 * x) is_poly_in x\",\"x = 1 / 5\", " ^
    "\"lhs (1 + -5 * x = 0) is_poly_in x\",\"lhs (1 + -5 * x = 0) has_degree_in x = 1\", " ^
    "\"1 / x = 5 is_ratequation_in x\"]");
 (*