removed unused fact collections
authorhaftmann
Tue Apr 16 19:50:21 2019 +0000 (7 days ago)
changeset 70176330382e284a4
parent 70175 85fb1a585f52
child 70177 b67bab2b132c
removed unused fact collections
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Rings.thy	Tue Apr 16 19:50:20 2019 +0000
     1.2 +++ b/src/HOL/Rings.thy	Tue Apr 16 19:50:21 2019 +0000
     1.3 @@ -1137,11 +1137,6 @@
     1.4      by (rule dvd_div_mult2_eq)
     1.5  qed
     1.6  
     1.7 -lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
     1.8 -  dvd_div_unit_iff unit_div_mult_swap unit_div_commute
     1.9 -  unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
    1.10 -  unit_eq_div1 unit_eq_div2
    1.11 -
    1.12  lemma is_unit_div_mult_cancel_left:
    1.13    assumes "a \<noteq> 0" and "is_unit b"
    1.14    shows "a div (a * b) = 1 div b"
    1.15 @@ -2520,20 +2515,6 @@
    1.16  
    1.17  end
    1.18  
    1.19 -text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
    1.20 -
    1.21 -lemmas mult_compare_simps =
    1.22 -  mult_le_cancel_right mult_le_cancel_left
    1.23 -  mult_le_cancel_right1 mult_le_cancel_right2
    1.24 -  mult_le_cancel_left1 mult_le_cancel_left2
    1.25 -  mult_less_cancel_right mult_less_cancel_left
    1.26 -  mult_less_cancel_right1 mult_less_cancel_right2
    1.27 -  mult_less_cancel_left1 mult_less_cancel_left2
    1.28 -  mult_cancel_right mult_cancel_left
    1.29 -  mult_cancel_right1 mult_cancel_right2
    1.30 -  mult_cancel_left1 mult_cancel_left2
    1.31 -
    1.32 -
    1.33  text \<open>Reasoning about inequalities with division\<close>
    1.34  
    1.35  context linordered_semidom