| changeset 44605 | 4877c4e184e5 |
| parent 31974 | e81979a703a4 |
| child 55380 | 4de48353034e |
--- a/src/FOL/ex/Natural_Numbers.thy Tue Aug 30 17:53:03 2011 +0200 +++ b/src/FOL/ex/Natural_Numbers.thy Tue Aug 30 18:12:48 2011 +0200 @@ -46,9 +46,8 @@ qed -definition - add :: "[nat, nat] => nat" (infixl "+" 60) where - "m + n = rec(m, n, \<lambda>x y. Suc(y))" +definition add :: "nat => nat => nat" (infixl "+" 60) + where "m + n = rec(m, n, \<lambda>x y. Suc(y))" lemma add_0 [simp]: "0 + n = n" unfolding add_def by (rule rec_0)