--- a/src/HOL/Word/WordGenLib.thy Mon Feb 16 19:35:52 2009 -0800
+++ b/src/HOL/Word/WordGenLib.thy Tue Feb 17 18:48:17 2009 +0100
@@ -293,9 +293,9 @@
shows "(x + y) mod b = z' mod b'"
proof -
from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
- by (simp add: zmod_zadd1_eq[symmetric])
+ by (simp add: mod_add_eq[symmetric])
also have "\<dots> = (x' + y') mod b'"
- by (simp add: zmod_zadd1_eq[symmetric])
+ by (simp add: mod_add_eq[symmetric])
finally show ?thesis by (simp add: 4)
qed