equal
deleted
inserted
replaced
147 nitpick [card = 2, expect = none] |
147 nitpick [card = 2, expect = none] |
148 by (rule Rep_sum_inverse) |
148 by (rule Rep_sum_inverse) |
149 |
149 |
150 lemma "0::nat \<equiv> Abs_Nat Zero_Rep" |
150 lemma "0::nat \<equiv> Abs_Nat Zero_Rep" |
151 nitpick [expect = none] |
151 nitpick [expect = none] |
152 by (rule Zero_nat_def_raw) |
152 by (rule Zero_nat_def [abs_def]) |
153 |
153 |
154 lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))" |
154 lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))" |
155 nitpick [expect = none] |
155 nitpick [expect = none] |
156 by (rule Nat.Suc_def) |
156 by (rule Nat.Suc_def) |
157 |
157 |