| 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