doc-src/TutorialI/Misc/Plus.thy

--- a/doc-src/TutorialI/Misc/Plus.thy	Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/Plus.thy	Thu May 29 22:45:33 2008 +0200
@@ -4,9 +4,8 @@
 
 text{*\noindent Define the following addition function *}
 
-consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-primrec
-"add m 0 = m"
+primrec add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"add m 0 = m" |
 "add m (Suc n) = add (Suc m) n"
 
 text{*\noindent and prove*}