--- a/src/HOL/Rat.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Rat.thy Wed Feb 17 21:51:57 2016 +0100
@@ -78,7 +78,7 @@
from \<open>q = Fract a b\<close> \<open>b \<noteq> 0\<close> \<open>?b \<noteq> 0\<close> have q: "q = Fract ?a ?b"
by (simp add: eq_rat dvd_div_mult mult.commute [of a])
from \<open>b \<noteq> 0\<close> have coprime: "coprime ?a ?b"
- by (auto intro: div_gcd_coprime_int)
+ by (auto intro: div_gcd_coprime)
show C proof (cases "b > 0")
case True
note assms
@@ -287,7 +287,7 @@
split:split_if_asm)
lemma normalize_coprime: "normalize r = (p, q) \<Longrightarrow> coprime p q"
- by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime_int
+ by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime
split:split_if_asm)
lemma normalize_stable [simp]: