diff -r 430d74089d4d -r 93c6f0da5c70 src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:04 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:05 2016 +0200
@@ -27,7 +27,7 @@
 begin
 
 lemma mod_0 [simp]: "0 mod a = 0"
-  using mod_div_equality [of 0 a] by simp
+  using div_mult_mod_eq [of 0 a] by simp
 
 lemma dvd_mod_iff: 
   assumes "k dvd n"
@@ -36,7 +36,7 @@
   from assms have "(k dvd m mod n) \<longleftrightarrow> (k dvd ((m div n) * n + m mod n))" 
     by (simp add: dvd_add_right_iff)
   also have "(m div n) * n + m mod n = m"
-    using mod_div_equality [of m n] by simp
+    using div_mult_mod_eq [of m n] by simp
   finally show ?thesis .
 qed
 
@@ -46,7 +46,7 @@
 proof -
   have "b dvd ((a div b) * b)" by simp
   also have "(a div b) * b = a"
-    using mod_div_equality [of a b] by (simp add: assms)
+    using div_mult_mod_eq [of a b] by (simp add: assms)
   finally show ?thesis .
 qed
 
@@ -72,7 +72,7 @@
   obtains s and t where "a = s * b + t" 
     and "euclidean_size t < euclidean_size b"
 proof -
-  from mod_div_equality [of a b] 
+  from div_mult_mod_eq [of a b] 
      have "a = a div b * b + a mod b" by simp
   with that and assms show ?thesis by (auto simp add: mod_size_less)
 qed
@@ -507,7 +507,7 @@
               (s' * a + t' * b) - r' div r * (s * a + t * b)" by (simp add: algebra_simps)
       also have "s' * a + t' * b = r'" by fact
       also have "s * a + t * b = r" by fact
-      also have "r' - r' div r * r = r' mod r" using mod_div_equality [of r' r]
+      also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r]
         by (simp add: algebra_simps)
       finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
     qed (auto simp: gcd_eucl_non_0 algebra_simps div_mod_equality')