| changeset 57514 | bdc2c6b40bf2 |
| parent 56154 | f0a927235162 |
| child 58881 | b9556a055632 |
--- a/src/HOL/Library/Numeral_Type.thy Sat Jul 05 10:09:01 2014 +0200 +++ b/src/HOL/Library/Numeral_Type.thy Sat Jul 05 11:01:53 2014 +0200 @@ -147,7 +147,7 @@ lemma of_nat_eq: "of_nat k = Abs (int k mod n)" apply (induct k) apply (simp add: zero_def) -apply (simp add: Rep_simps add_def one_def zmod_simps add_ac) +apply (simp add: Rep_simps add_def one_def zmod_simps ac_simps) done lemma of_int_eq: "of_int z = Abs (z mod n)"