| changeset 46082 | 1c436a920730 |
| parent 45970 | b6d0cff57d96 |
| child 46547 | d1dcb91a512e |
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Jan 03 18:33:17 2012 +0100 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Tue Jan 03 18:33:17 2012 +0100 @@ -163,10 +163,6 @@ nitpick [expect = none] by (rule Rep_Nat_inverse) -lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})" -(*nitpick [card = 1, unary_ints, max_potential = 0, expect = none] (?)*) -by (rule Zero_int_def_raw) - lemma "Abs_list (Rep_list a) = a" nitpick [card = 1\<emdash>2, expect = none] by (rule Rep_list_inverse)