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 \ fst x = 0 \ 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 \ snd (quot_of_fract x) = 1" by transfer auto