| changeset 46905 | 6b1c0a80a57a |
| parent 46547 | d1dcb91a512e |
| child 47908 | 25686e1e0024 |
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Mar 13 16:40:06 2012 +0100 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Mar 13 16:56:56 2012 +0100 @@ -149,7 +149,7 @@ lemma "0::nat \<equiv> Abs_Nat Zero_Rep" nitpick [expect = none] -by (rule Zero_nat_def_raw) +by (rule Zero_nat_def [abs_def]) lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))" nitpick [expect = none]