# HG changeset patch
# User haftmann
# Date 1510828223 -3600
# Node ID 6a85b8a9c28c89a1e43ecba003e8e40f060ec411
# Parent  8fa951baba0dd3cad3543dc33da2f95664f4997d
removed overambitious simp rules from e7e54a0b9197

diff -r 8fa951baba0d -r 6a85b8a9c28c src/HOL/Computational_Algebra/Normalized_Fraction.thy
--- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Tue Nov 14 23:07:47 2017 +0100
+++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Thu Nov 16 11:30:23 2017 +0100
@@ -20,7 +20,7 @@
   "normalize_quot (a, 0) = (0, 1)"
   by (simp add: normalize_quot_def)
 
-lemma normalize_quot_proj [simp]:
+lemma normalize_quot_proj:
   "fst (normalize_quot (a, b)) = a div (gcd a b * unit_factor b)"
   "snd (normalize_quot (a, b)) = normalize b div gcd a b" if "b \<noteq> 0"
   using that by (simp_all add: normalize_quot_def Let_def mult.commute [of _ "unit_factor b"] dvd_div_mult2_eq mult_unit_dvd_iff')
@@ -275,8 +275,7 @@
   have "coprime a' b'" by (simp add: a'_def b'_def coprime_normalize_quot)
   thus "(b' div unit_factor a', a' div unit_factor a') \<in> normalized_fracts"
     using assms(1,2) d
-    by (auto simp: normalized_fracts_def ac_simps)
-      (metis gcd.normalize_left_idem gcd_div_unit2 is_unit_gcd unit_factor_is_unit)
+    by (auto simp add: normalized_fracts_def ac_simps dvd_div_unit_iff elim: coprime_imp_coprime)
 qed fact+
   
 lemma quot_of_fract_inverse: