
diff -r d3d508b23d1d -r 960509bfd47e src/HOL/Computational_Algebra/Normalized_Fraction.thy
--- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Thu Oct 19 17:16:13 2017 +0100
+++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Fri Oct 20 07:46:10 2017 +0200
@@ -239,7 +239,6 @@
   
 lemma normalize_quot_eq_0_iff [simp]: "fst (normalize_quot x) = 0 \<longleftrightarrow> fst x = 0 \<or> snd x = 0"
   by (auto simp: normalize_quot_def case_prod_unfold Let_def div_mult_unit2 dvd_div_eq_0_iff)
-  find_theorems "_ div _ = 0"
   
 lemma fst_quot_of_fract_0_imp: "fst (quot_of_fract x) = 0 \<Longrightarrow> snd (quot_of_fract x) = 1"
   by transfer auto




