--- a/src/FOL/ex/Nat_Class.thy Tue Aug 30 17:53:03 2011 +0200
+++ b/src/FOL/ex/Nat_Class.thy Tue Aug 30 18:12:48 2011 +0200
@@ -26,9 +26,8 @@
and rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
begin
-definition
- add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 60) where
- "m + n = rec(m, n, \<lambda>x y. Suc(y))"
+definition add :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 60)
+ where "m + n = rec(m, n, \<lambda>x y. Suc(y))"
lemma Suc_n_not_n: "Suc(k) \<noteq> (k::'a)"
apply (rule_tac n = k in induct)
--- 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)