src/HOL/Algebra/IntRing.thy
changeset 29948 cdf12a1cb963
parent 29700 22faf21db3df
child 30729 461ee3e49ad3
--- a/src/HOL/Algebra/IntRing.thy	Mon Feb 16 19:35:52 2009 -0800
+++ b/src/HOL/Algebra/IntRing.thy	Tue Feb 17 18:48:17 2009 +0100
@@ -407,7 +407,7 @@
 
   hence "b mod m = (x * m + a) mod m" by simp
   also
-      have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq)
+      have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: mod_add_eq)
   also
       have "\<dots> = a mod m" by simp
   finally