# HG changeset patch
# User haftmann
# Date 1555444221 0
# Node ID 330382e284a4a14a7f0582e029e29883c83e2189
# Parent  85fb1a585f52150a27a81603240e8df4e615d09c
removed unused fact collections

diff -r 85fb1a585f52 -r 330382e284a4 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue Apr 16 19:50:20 2019 +0000
+++ b/src/HOL/Rings.thy	Tue Apr 16 19:50:21 2019 +0000
@@ -1137,11 +1137,6 @@
     by (rule dvd_div_mult2_eq)
 qed
 
-lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
-  dvd_div_unit_iff unit_div_mult_swap unit_div_commute
-  unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
-  unit_eq_div1 unit_eq_div2
-
 lemma is_unit_div_mult_cancel_left:
   assumes "a \<noteq> 0" and "is_unit b"
   shows "a div (a * b) = 1 div b"
@@ -2520,20 +2515,6 @@
 
 end
 
-text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
-
-lemmas mult_compare_simps =
-  mult_le_cancel_right mult_le_cancel_left
-  mult_le_cancel_right1 mult_le_cancel_right2
-  mult_le_cancel_left1 mult_le_cancel_left2
-  mult_less_cancel_right mult_less_cancel_left
-  mult_less_cancel_right1 mult_less_cancel_right2
-  mult_less_cancel_left1 mult_less_cancel_left2
-  mult_cancel_right mult_cancel_left
-  mult_cancel_right1 mult_cancel_right2
-  mult_cancel_left1 mult_cancel_left2
-
-
 text \<open>Reasoning about inequalities with division\<close>
 
 context linordered_semidom