diff -r 0e69700b70d6 -r f15995595411 src/Tools/isac/Knowledge/Base_Tools.thy
--- a/src/Tools/isac/Knowledge/Base_Tools.thy	Thu Apr 29 17:08:38 2021 +0200
+++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Sun May 02 13:13:44 2021 +0200
@@ -5,19 +5,20 @@
                       (*  ^^^ for KEStore_Elems.add_thes *)
 begin
 subsection \<open>theorems for Base_Tools\<close>
+
+lemma real_unari_minus:   "- a = (-1) * (a::real)" by auto
+(*Semiring_Normalization.comm_ring_1_class.ring_normalization_rules(1)*)
+
+(* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)
+lemma radd_left_cancel_le: "((k::real) + m <= k + n) = (m <= n)" by auto
+(*Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_left*)
+
 axiomatization where (*for evaluating the assumptions of conditional rules*)
+  (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)
+  rat_leq1: "[| 0 \<noteq> b; 0 \<noteq> d |] ==> (a / b <= c / d) = (a * d <= b * c)"(*Quickcheck found a counterexample*) and
+  rat_leq2:	          "0 \<noteq> d    ==> (a     <= c / d) = (a * d <=     c)" (*Quickcheck found a counterexample*) and
+  rat_leq3:	   "0 \<noteq> b           ==> (a / b <= c    ) = (a     <= b * c)" (*Quickcheck found a counterexample*)
 
-(*last_thmI:	        "lastI (x#xs) = (if xs =!= [] then x else lastI xs)" and*)
-  real_unari_minus:   "- a = (-1) * a" and
-  radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)" and
-  (* should be in Rational.thy, but: 
-   needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML...*)
-  rat_leq1:	      "[| b ~= 0; d ~= 0 |] ==>
-		       ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*) and
-  rat_leq2:	      "d ~= 0 ==>
-		       ( a      <= (c / d)) = ((a*d) <=    c )"(*Isa?*) and
-  rat_leq3:	      "b ~= 0 ==>
-		       ((a / b) <=  c     ) = ( a    <= (b*c))"(*Isa?*)
 
 subsection \<open>setup for ML-functions\<close>
 text \<open>required by "eval_binop" below\<close>