changeset 55642 | 63beb38e9258 |
parent 55428 | 0ab52bf7b5e6 |
child 55736 | f1ed1e9cd080 |
--- a/src/HOL/Code_Numeral.thy Fri Feb 21 00:09:55 2014 +0100 +++ b/src/HOL/Code_Numeral.thy Fri Feb 21 00:09:56 2014 +0100 @@ -888,7 +888,7 @@ "case_natural f g n = (if n = 0 then f else g (n - 1))" by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def) -declare natural.recs [code del] +declare natural.rec [code del] lemma [code abstract]: "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n"