| changeset 46905 | 6b1c0a80a57a |
| parent 46879 | a8b1236e0837 |
| child 47108 | 2a1953f0d20d |
--- a/src/HOL/Import/HOL_Light/HOLLightInt.thy Tue Mar 13 16:40:06 2012 +0100 +++ b/src/HOL/Import/HOL_Light/HOLLightInt.thy Tue Mar 13 16:56:56 2012 +0100 @@ -90,7 +90,7 @@ lemma int_mod_def': "int_mod = (\<lambda>u ua ub. (u dvd (ua - ub)))" - by (simp add: int_mod_def_raw) + by (simp add: int_mod_def [abs_def]) lemma int_congruent: "\<forall>x xa xb. int_mod xb x xa = (\<exists>d. x - xa = xb * d)"