1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Sun May 02 13:13:44 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Sun May 02 15:55:37 2021 +0200
     1.3 @@ -10,14 +10,16 @@
     1.4  (*Semiring_Normalization.comm_ring_1_class.ring_normalization_rules(1)*)
     1.5  
     1.6  (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)
     1.7 -lemma radd_left_cancel_le: "((k::real) + m <= k + n) = (m <= n)" by auto
     1.8 +lemma radd_left_cancel_le: "((k::real) + m \<le> k + n) = (m \<le> n)" by auto
     1.9  (*Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_left*)
    1.10  
    1.11 +thm "Fields.linordered_field_class.mult_imp_le_div_pos" (*0 < ?y \<Longrightarrow> ?z * ?y \<le> ?x \<Longrightarrow> ?z \<le> ?x / ?y*)
    1.12 +
    1.13  axiomatization where (*for evaluating the assumptions of conditional rules*)
    1.14    (* should be in Rational.thy, but needed for asms in e.g. d2_pqformula1 in PolyEq, RootEq... *)
    1.15 -  rat_leq1: "[| 0 \<noteq> b; 0 \<noteq> d |] ==> (a / b <= c / d) = (a * d <= b * c)"(*Quickcheck found a counterexample*) and
    1.16 -  rat_leq2:	          "0 \<noteq> d    ==> (a     <= c / d) = (a * d <=     c)" (*Quickcheck found a counterexample*) and
    1.17 -  rat_leq3:	   "0 \<noteq> b           ==> (a / b <= c    ) = (a     <= b * c)" (*Quickcheck found a counterexample*)
    1.18 +  rat_leq1: "0 \<noteq> b \<Longrightarrow> 0 \<noteq> d \<Longrightarrow> (a / b \<le> c / d) = (a * d \<le> b * c)"(*Quickcheck found a counterexample*) and
    1.19 +  rat_leq2:	          "0 \<noteq> d \<Longrightarrow> (a     \<le> c / d) = (a * d \<le>     c)"(*Quickcheck found a counterexample*) and
    1.20 +  rat_leq3:	"0 \<noteq> b           \<Longrightarrow> (a / b \<le> c    ) = (a     \<le> b * c)"(*Quickcheck found a counterexample*)
    1.21  
    1.22  
    1.23  subsection \<open>setup for ML-functions\<close>