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