author wenzelm Sat, 11 Mar 2006 17:30:35 +0100 changeset 19249 86c73395c99b parent 19248 25bb0a883ac5 child 19250 932a50e2332f
--- a/doc-src/TutorialI/Misc/Plus.thy	Sat Mar 11 17:24:37 2006 +0100
+++ b/doc-src/TutorialI/Misc/Plus.thy	Sat Mar 11 17:30:35 2006 +0100
@@ -4,18 +4,18 @@

text{*\noindent Define the following addition function *}

-consts plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
primrec
-"plus m 0 = m"
-"plus m (Suc n) = plus (Suc m) n"

text{*\noindent and prove*}
(*<*)
-lemma [simp]: "!m. plus m n = m+n"
+lemma [simp]: "!m. add m n = m+n"
apply(induct_tac n)
by(auto)
(*>*)
-lemma "plus m n = m+n"
+lemma "add m n = m+n"
(*<*)
by(simp)

--- a/doc-src/TutorialI/Misc/document/Plus.tex	Sat Mar 11 17:24:37 2006 +0100
+++ b/doc-src/TutorialI/Misc/document/Plus.tex	Sat Mar 11 17:30:35 2006 +0100
@@ -20,11 +20,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isamarkupfalse%
-\ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
+\ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
\isanewline
-{\isachardoublequoteopen}plus\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ plus\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n{\isachardoublequoteclose}%
\endisadelimproof