# HG changeset patch
# User wenzelm
# Date 1142094635 -3600
# Node ID 86c73395c99bf368db2ab60e9661a633c7e4a309
# Parent  25bb0a883ac58a6473cb82eca61cd72896edb91a
renamed plus to add;

diff -r 25bb0a883ac5 -r 86c73395c99b doc-src/TutorialI/Misc/Plus.thy
--- 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"
+"add m 0 = m"
+"add m (Suc n) = add (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)
 
diff -r 25bb0a883ac5 -r 86c73395c99b doc-src/TutorialI/Misc/document/Plus.tex
--- 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\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}plus\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ plus\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n{\isachardoublequoteclose}%
+{\isachardoublequoteopen}add\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
+{\isachardoublequoteopen}add\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ add\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 \noindent and prove%
 \end{isamarkuptext}%
@@ -43,7 +43,7 @@
 %
 \endisadelimproof
 \isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequoteclose}%
+\ {\isachardoublequoteopen}add\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequoteclose}%
 \isadelimproof
 %
 \endisadelimproof