# HG changeset patch
# User paulson
# Date 1121260753 -7200
# Node ID 6109d4020420b3259af01be8c580baae7f3748cc
# Parent  140f1e0ea846852970f4a065933b885556835fb3
auto update

diff -r 140f1e0ea846 -r 6109d4020420 doc-src/TutorialI/Misc/document/natsum.tex
--- 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}%
diff -r 140f1e0ea846 -r 6109d4020420 doc-src/TutorialI/Recdef/document/simplification.tex
--- 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%
diff -r 140f1e0ea846 -r 6109d4020420 doc-src/TutorialI/isabellesym.sty
--- 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}}