doc-src/TutorialI/Recdef/document/simplification.tex

--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Thu Nov 09 11:58:43 2006 +0100
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Thu Nov 09 11:58:45 2006 +0100
@@ -47,17 +47,17 @@
 condition simplifies to \isa{True} or \isa{False}.  For
 example, simplification reduces
 \begin{isabelle}%
-\ \ \ \ \ simplification{\isachardot}gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k%
+\ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k%
 \end{isabelle}
 in one step to
 \begin{isabelle}%
-\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ m\ else\ simplification{\isachardot}gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
+\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
 \end{isabelle}
 where the condition cannot be reduced further, and splitting leads to
 \begin{isabelle}%
-\ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ simplification{\isachardot}gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
+\ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
 \end{isabelle}
-Since the recursive call \isa{simplification{\isachardot}gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by
+Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by
 an \isa{if}, it is unfolded again, which leads to an infinite chain of
 simplification steps. Fortunately, this problem can be avoided in many
 different ways.
@@ -69,7 +69,7 @@
 \isa{if} is involved.
 
 If possible, the definition should be given by pattern matching on the left
-rather than \isa{if} on the right. In the case of \isa{simplification{\isachardot}gcd} the
+rather than \isa{if} on the right. In the case of \isa{gcd} the
 following alternative definition suggests itself:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -100,7 +100,7 @@
 always available.
 
 A final alternative is to replace the offending simplification rules by
-derived conditional ones. For \isa{simplification{\isachardot}gcd} it means we have to prove
+derived conditional ones. For \isa{gcd} it means we have to prove
 these lemmas:%
 \end{isamarkuptext}%
 \isamarkuptrue%