# HG changeset patch
# User wenzelm
# Date 1314720768 -7200
# Node ID 4877c4e184e56eacdd9fd92001bb4bd86d41b450
# Parent  1ad3159323dc816b282781a6dd57cb23314f0bb9
tuned document;

diff -r 1ad3159323dc -r 4877c4e184e5 src/FOL/ex/Nat_Class.thy
--- 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)
diff -r 1ad3159323dc -r 4877c4e184e5 src/FOL/ex/Natural_Numbers.thy
--- 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)