--- a/doc-src/TutorialI/Misc/document/natsum.tex Wed Jul 13 15:06:20 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Wed Jul 13 15:19:13 2005 +0200
@@ -91,7 +91,7 @@
\begin{isamarkuptext}%
\noindent
For efficiency's sake, this built-in prover ignores quantified formulae,
-logical connectives, and all arithmetic operations apart from addition.
+many logical connectives, and all arithmetic operations apart from addition.
In consequence, \isa{auto} and \isa{simp} cannot prove this slightly more complex goal:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -135,7 +135,7 @@
\isa{k}~\sdx{dvd} are also supported, where the former two are eliminated
by case distinctions, again blowing up the running time.
-If the formula involves explicit quantifiers, \isa{arith} may take
+If the formula involves quantifiers, \isa{arith} may take
super-exponential time and space.
\end{warn}%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Recdef/document/simplification.tex Wed Jul 13 15:06:20 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Wed Jul 13 15:19:13 2005 +0200
@@ -35,17 +35,17 @@
condition simplifies to \isa{True} or \isa{False}. For
example, simplification reduces
\begin{isabelle}%
-\ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k%
+\ \ \ \ \ simplification{\isachardot}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\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
+\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ m\ else\ simplification{\isachardot}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}\ 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}\ simplification{\isachardot}gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
\end{isabelle}
-Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by
+Since the recursive call \isa{simplification{\isachardot}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.
@@ -57,7 +57,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{gcd} the
+rather than \isa{if} on the right. In the case of \isa{simplification{\isachardot}gcd} the
following alternative definition suggests itself:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -88,7 +88,7 @@
always available.
A final alternative is to replace the offending simplification rules by
-derived conditional ones. For \isa{gcd} it means we have to prove
+derived conditional ones. For \isa{simplification{\isachardot}gcd} it means we have to prove
these lemmas:%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/TutorialI/isabellesym.sty Wed Jul 13 15:06:20 2005 +0200
+++ b/doc-src/TutorialI/isabellesym.sty Wed Jul 13 15:19:13 2005 +0200
@@ -359,3 +359,4 @@
\newcommand{\isasymcedilla}{\isatext{\c\relax}}
\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
\newcommand{\isasymspacespace}{\isamath{~~}}
+\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}