updated;

--- a/doc-src/IsarOverview/Isar/document/isabelle.sty	Thu Jun 09 12:04:53 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/isabelle.sty	Thu Jun 09 12:06:38 2005 +0200
@@ -3,6 +3,7 @@
 %%
 %% macros for Isabelle generated LaTeX output
 %%
+%% $Id$
 
 %%% Simple document preparation (based on theory token language and symbols)
 

--- a/doc-src/IsarOverview/Isar/document/isabellesym.sty	Thu Jun 09 12:04:53 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/isabellesym.sty	Thu Jun 09 12:06:38 2005 +0200
@@ -3,6 +3,7 @@
 %%
 %% definitions of standard Isabelle symbols
 %%
+%% $Id$
 
 % symbol definitions
 
@@ -219,6 +220,7 @@
 \newcommand{\isasymOr}{\isamath{\bigvee}}
 \newcommand{\isasymforall}{\isamath{\forall\,}}
 \newcommand{\isasymexists}{\isamath{\exists\,}}
+\newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb
 \newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
 \newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
 \newcommand{\isasymturnstile}{\isamath{\vdash}}

--- a/doc-src/IsarOverview/Isar/document/pdfsetup.sty	Thu Jun 09 12:04:53 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/pdfsetup.sty	Thu Jun 09 12:06:38 2005 +0200
@@ -3,6 +3,7 @@
 %%
 %% smart url or hyperref setup
 %%
+%% $Id$
 
 \@ifundefined{pdfoutput}
 {\usepackage{url}}

--- a/doc-src/TutorialI/Types/document/Axioms.tex	Thu Jun 09 12:04:53 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Axioms.tex	Thu Jun 09 12:06:38 2005 +0200
@@ -49,8 +49,22 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}parord{\isacharparenright}\ {\isacharless}{\isacharless}\ y\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+The conclusion is not just \isa{{\isasymnot}\ y\ {\isacharless}{\isacharless}\ x} because the 
+simplifier's preprocessor (see \S\ref{sec:simp-preprocessor})
+would turn it into \isa{{\isacharparenleft}y\ {\isacharless}{\isacharless}\ x{\isacharparenright}\ {\isacharequal}\ False}, yielding
+a nonterminating rewrite rule.  
+(It would be used to try to prove its own precondition \emph{ad
+    infinitum}.)
+In the form above, the rule is useful.
+The type constraint is necessary because otherwise Isabelle would only assume
+\isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel} (as required in the type of \isa{{\isacharless}{\isacharless}}), 
+when the proposition is not a theorem.  The proof is easy:%
+\end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le\ antisym{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 We could now continue in this vein and develop a whole theory of
@@ -62,10 +76,26 @@
 \isamarkuptrue%
 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ parord\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{apply}\ intro{\isacharunderscore}classes\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+This time \isa{intro{\isacharunderscore}classes} leaves us with the four axioms,
+specialized to type \isa{bool}, as subgoals:
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}bool{\isachardot}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ x\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}bool{\isacharparenright}\ z{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ z\isanewline
+\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ y\isanewline
+\ {\isadigit{4}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}bool{\isacharparenright}\ y{\isasymColon}bool{\isachardot}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}%
+\end{isabelle}
+Fortunately, the proof is easy for \isa{blast}
+once we have unfolded the definitions
+of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} at type \isa{bool}:%
+\end{isamarkuptxt}%
 \isamarkuptrue%
+\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ only{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def\ less{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -76,7 +106,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}P{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isacharless}{\isacharless}\ Q\ {\isasymLongrightarrow}\ {\isasymnot}{\isacharparenleft}Q\ {\isacharless}{\isacharless}\ P{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ simp\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -108,10 +138,13 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}linord{\isachardot}\ x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}\ x{\isachardoublequote}\isanewline
 \isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline
 \isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}insert\ linear{\isacharparenright}\isanewline
 \isamarkupfalse%
+\isacommand{apply}\ blast\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 Linear orders are an example of subclassing\index{subclasses}
@@ -145,12 +178,28 @@
 \isamarkuptrue%
 \isacommand{instance}\ parord\ {\isacharless}\ strord\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
-\isamarkuptrue%
+\isacommand{apply}\ intro{\isacharunderscore}classes\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymnot}\ x\ {\isacharless}{\isacharless}\ x\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}{\isacharprime}a{\isacharparenright}\ z{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z\isanewline
+\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}a{\isachardot}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}\isanewline
+type\ variables{\isacharcolon}\isanewline
+\isaindent{\ \ }{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord%
+\end{isabelle}
+Assuming \isa{{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord}, the three axioms of class \isa{strord}
+are easily proved:%
+\end{isamarkuptxt}%
+\ \ \isamarkuptrue%
+\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline
+\ \isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trans\ antisym{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ refl{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 The subclass relation must always be acyclic. Therefore Isabelle will

--- a/doc-src/TutorialI/Types/document/Numbers.tex	Thu Jun 09 12:04:53 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Thu Jun 09 12:06:38 2005 +0200
@@ -5,15 +5,23 @@
 \isacommand{theory}\ Numbers\ {\isacharequal}\ Real{\isacharcolon}\isanewline
 \isanewline
 \isamarkupfalse%
+\isacommand{ML}\ {\isachardoublequote}Pretty{\isachardot}setmargin\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{ML}\ {\isachardoublequote}IsarOutput{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 numeric literals; default simprules; can re-orient%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m%
+\end{isabelle}%
+\end{isamarkuptxt}%
 \isamarkuptrue%
+\isacommand{oops}\isanewline
 \isanewline
 \isamarkupfalse%
 \isacommand{consts}\ h\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
@@ -67,10 +75,23 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}i\ {\isacharplus}\ j{\isacharasterisk}l{\isacharasterisk}k\ {\isacharplus}\ m{\isacharasterisk}n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n{\isacharasterisk}m\ {\isacharplus}\ i\ {\isacharplus}\ k{\isacharasterisk}j{\isacharasterisk}l{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ j\ {\isacharasterisk}\ l\ {\isacharasterisk}\ k\ {\isacharplus}\ m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n\ {\isacharasterisk}\ m\ {\isacharplus}\ i\ {\isacharplus}\ k\ {\isacharasterisk}\ j\ {\isacharasterisk}\ l{\isacharparenright}%
+\end{isabelle}%
+\end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
+\isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ add{\isacharunderscore}ac\ mult{\isacharunderscore}ac{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ }f\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}%
+\end{isabelle}%
+\end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
+\isacommand{oops}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \begin{isabelle}%
@@ -96,16 +117,33 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
+\isacommand{apply}\ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split\ iff\ del{\isacharcolon}\ less{\isacharunderscore}Suc{\isadigit{0}}{\isacharparenright}\isanewline
+\ %
+\isamarkupcmt{\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ Suc\ {\isadigit{0}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ Suc\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}%
+\end{isabelle}%
+}
+\isanewline
 \isamarkupfalse%
+\isacommand{apply}\ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}n{\isacharequal}{\isadigit{0}}{\isachardoublequote}{\isacharcomma}\ force{\isacharcomma}\ arith{\isacharparenright}\isanewline
 \isamarkupfalse%
+\isacommand{done}\isanewline
 \isanewline
 \isanewline
 \isamarkupfalse%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{4}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{apply}\ {\isacharparenleft}simp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharcomma}\ clarify{\isacharparenright}\isanewline
+\ %
+\isamarkupcmt{\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ {\isadigit{4}}\ {\isacharplus}\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}%
+\end{isabelle}%
+}
+\isanewline
 \isamarkupfalse%
+\isacommand{apply}\ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}n{\isacharequal}{\isadigit{0}}\ {\isacharbar}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}{\isacharcomma}\ force{\isacharcomma}\ arith{\isacharparenright}\isanewline
 \isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \begin{isabelle}%
@@ -226,11 +264,12 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}x{\isacharplus}y{\isacharparenright}\ {\isasymle}\ abs\ x\ {\isacharplus}\ abs\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
+\isacommand{by}\ arith\isanewline
 \isanewline
 \isamarkupfalse%
 \isacommand{lemma}\ {\isachardoublequote}abs\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}x{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ abs\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ zabs{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 Induction rules for the Integers
@@ -305,19 +344,45 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isadigit{3}}{\isacharslash}{\isadigit{4}}\ {\isacharless}\ {\isacharparenleft}{\isadigit{7}}{\isacharslash}{\isadigit{8}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
+\isacommand{by}\ simp\ \isanewline
 \isanewline
 \isamarkupfalse%
 \isacommand{lemma}\ {\isachardoublequote}P\ {\isacharparenleft}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ P\ {\isacharparenleft}{\isadigit{3}}\ {\isacharslash}\ {\isadigit{4}}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}\ {\isacharslash}\ {\isadigit{1}}{\isadigit{5}}{\isacharparenright}{\isacharparenright}%
+\end{isabelle}%
+\end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
+\isacommand{apply}\ simp\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ P\ {\isacharparenleft}{\isadigit{2}}\ {\isacharslash}\ {\isadigit{5}}{\isacharparenright}%
+\end{isabelle}%
+\end{isamarkuptxt}%
 \isamarkuptrue%
+\isacommand{oops}\isanewline
 \isanewline
 \isamarkupfalse%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isadigit{3}}\ {\isacharslash}\ {\isadigit{4}}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}\ {\isacharslash}\ {\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ x%
+\end{isabelle}%
+\end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
+\isacommand{apply}\ simp\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharless}\ x\ {\isacharasterisk}\ {\isadigit{5}}%
+\end{isabelle}%
+\end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
+\isacommand{oops}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 Ring and Field
@@ -345,7 +410,7 @@
 \rulename{field_mult_cancel_right}%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
+\isacommand{ML}{\isacharbraceleft}{\isacharasterisk}set\ show{\isacharunderscore}sorts{\isacharasterisk}{\isacharbraceright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 effect of show sorts on the above
@@ -357,7 +422,7 @@
 \rulename{field_mult_cancel_right}%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
+\isacommand{ML}{\isacharbraceleft}{\isacharasterisk}reset\ show{\isacharunderscore}sorts{\isacharasterisk}{\isacharbraceright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 absolute value

--- a/doc-src/TutorialI/Types/document/Overloading.tex	Thu Jun 09 12:04:53 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading.tex	Thu Jun 09 12:06:38 2005 +0200
@@ -4,7 +4,7 @@
 \isamarkupfalse%
 \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}ordrel\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ intro{\isacharunderscore}classes\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent

--- a/doc-src/TutorialI/Types/document/Overloading1.tex	Thu Jun 09 12:04:53 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex	Thu Jun 09 12:06:38 2005 +0200
@@ -41,8 +41,16 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+Command \isacommand{instance} actually starts a proof, namely that
+\isa{bool} satisfies all axioms of \isa{ordrel}.
+There are none, but we still need to finish that proof, which we do
+by invoking the \methdx{intro_classes} method:%
+\end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
+\isacommand{by}\ intro{\isacharunderscore}classes\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -64,7 +72,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ P{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent

--- a/doc-src/TutorialI/Types/document/Overloading2.tex	Thu Jun 09 12:04:53 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Thu Jun 09 12:06:38 2005 +0200
@@ -12,6 +12,7 @@
 \isamarkuptrue%
 \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
 \isamarkupfalse%
+\isacommand{by}\ intro{\isacharunderscore}classes\isanewline
 \isanewline
 \isamarkupfalse%
 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline

--- a/doc-src/TutorialI/Types/document/Pairs.tex	Thu Jun 09 12:04:53 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Pairs.tex	Thu Jun 09 12:06:38 2005 +0200
@@ -67,7 +67,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}x{\isacharparenright}\ p\ {\isacharequal}\ fst\ p{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 This works well if rewriting with \isa{split{\isacharunderscore}def} finishes the
@@ -90,12 +90,19 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}y{\isacharparenright}\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}split{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymforall}x\ y{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymlongrightarrow}\ y\ {\isacharequal}\ snd\ p%
+\end{isabelle}
+This subgoal is easily proved by simplification. Thus we could have combined
+simplification and splitting in one command that proves the goal outright:%
+\end{isamarkuptxt}%
 \isamarkuptrue%
-\isanewline
 \isamarkupfalse%
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ split{\isacharunderscore}split{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 Let us look at a second example:%
@@ -103,15 +110,42 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}let\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ p\ in\ fst\ p\ {\isacharequal}\ x{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ fst\ p\ {\isacharequal}\ x{\isacharparenright}\ p%
+\end{isabelle}
+A paired \isa{let} reduces to a paired $\lambda$-abstraction, which
+can be split as above. The same is true for paired set comprehension:%
+\end{isamarkuptxt}%
 \isamarkuptrue%
 \isamarkupfalse%
 \isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{apply}\ simp\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ split\ op\ {\isacharequal}\ p\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p%
+\end{isabelle}
+Again, simplification produces a term suitable for \isa{split{\isacharunderscore}split}
+as above. If you are worried about the strange form of the premise:
+\isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x\ {\isacharequal}\ y} is short for \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y}.
+The same proof procedure works for%
+\end{isamarkuptxt}%
 \isamarkuptrue%
 \isamarkupfalse%
 \isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymLongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+except that we now have to use \isa{split{\isacharunderscore}split{\isacharunderscore}asm}, because
+\isa{split} occurs in the assumptions.
+
+However, splitting \isa{split} is not always a solution, as no \isa{split}
+may be present in the goal. Consider the following function:%
+\end{isamarkuptxt}%
 \isamarkuptrue%
 \isamarkupfalse%
 \isacommand{consts}\ swap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isachardoublequote}\isanewline
@@ -126,16 +160,51 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ p{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+simplification will do nothing, because the defining equation for \isa{Pairs{\isachardot}swap}
+expects a pair. Again, we need to turn \isa{p} into a pair first, but this
+time there is no \isa{split} in sight. In this case the only thing we can do
+is to split the term by hand:%
+\end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ p{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymLongrightarrow}\ Pairs{\isachardot}swap\ {\isacharparenleft}Pairs{\isachardot}swap\ p{\isacharparenright}\ {\isacharequal}\ p%
+\end{isabelle}
+Again, \methdx{case_tac} is applicable because \isa{{\isasymtimes}} is a datatype.
+The subgoal is easily proved by \isa{simp}.
+
+Splitting by \isa{case{\isacharunderscore}tac} also solves the previous examples and may thus
+appear preferable to the more arcane methods introduced first. However, see
+the warning about \isa{case{\isacharunderscore}tac} in \S\ref{sec:struct-ind-case}.
+
+In case the term to be split is a quantified variable, there are more options.
+You can split \emph{all} \isa{{\isasymAnd}}-quantified variables in a goal
+with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:%
+\end{isamarkuptxt}%
 \isamarkuptrue%
 \isamarkupfalse%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}p\ q{\isachardot}\ swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ q\ {\isasymlongrightarrow}\ p\ {\isacharequal}\ q{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b\ aa\ ba{\isachardot}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }Pairs{\isachardot}swap\ {\isacharparenleft}Pairs{\isachardot}swap\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}%
+\end{isabelle}%
+\end{isamarkuptxt}%
 \isamarkuptrue%
+\isacommand{apply}\ simp\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -150,7 +219,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -161,7 +230,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}p{\isachardot}\ {\isasymexists}q{\isachardot}\ swap\ p\ {\isacharequal}\ swap\ q{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ simp\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent

--- a/doc-src/TutorialI/Types/document/Records.tex	Thu Jun 09 12:04:53 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Records.tex	Thu Jun 09 12:06:38 2005 +0200
@@ -77,7 +77,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
 \ \ \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ simp\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 The \emph{update}\index{update!record} operation is functional.  For
@@ -88,7 +88,7 @@
 \isacommand{lemma}\ {\isachardoublequote}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isasymrparr}\ {\isacharequal}\isanewline
 \ \ \ \ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{0}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}\isanewline
 \ \ \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ simp\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \begin{warn}
@@ -139,7 +139,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ p{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
 \ \ \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ simp\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 This lemma applies to any record whose first two fields are \isa{Xcoord} and~\isa{Ycoord}.  Note that \isa{{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}} is exactly the same as \isa{{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}}.  Selectors and updates are always polymorphic wrt.\ the
@@ -152,7 +152,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}point{\isachardot}more\ cpt{\isadigit{1}}\ {\isacharequal}\ {\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}{\isachardoublequote}\isanewline
 \ \ \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ cpt{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 We see that the colour part attached to this \isa{point} is a
@@ -167,7 +167,7 @@
   \medskip
   \begin{tabular}{l}
   \isa{point}~\isa{{\isacharequal}}~\isa{point} \\
-  \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a{\isasymrparr}} \\
+  \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}~\isa{{\isacharequal}}~\isa{{\isacharprime}a\ point{\isacharunderscore}scheme} \\
   \end{tabular}
   \medskip
 
@@ -204,7 +204,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}incX\ r\ {\isacharequal}\ setX\ r\ {\isacharparenleft}getX\ r\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ getX{\isacharunderscore}def\ setX{\isacharunderscore}def\ incX{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \begin{warn}
@@ -231,7 +231,7 @@
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharprime}{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharprime}{\isasymrparr}{\isacharparenright}\ {\isacharequal}\isanewline
 \ \ \ \ {\isacharparenleft}a\ {\isacharequal}\ a{\isacharprime}\ {\isasymand}\ b\ {\isacharequal}\ b{\isacharprime}{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ simp\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 The following equality is similar, but generic, in that \isa{r}
@@ -240,7 +240,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Ycoord\ {\isacharcolon}{\isacharequal}\ b{\isacharcomma}\ Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequote}\isanewline
 \ \ \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ simp\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 We see above the syntax for iterated updates.  We could equivalently
@@ -253,7 +253,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isasymrparr}{\isachardoublequote}\isanewline
 \ \ \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ simp\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 The generic version of this equality includes the pseudo-field
@@ -262,7 +262,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord\ r{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord\ r{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ point{\isachardot}more\ r{\isasymrparr}{\isachardoublequote}\isanewline
 \ \ \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ simp\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \medskip The simplifier can prove many record equalities
@@ -272,8 +272,9 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isanewline
 \ \ \isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
+\isacommand{apply}\ simp{\isacharquery}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{oops}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 Here the simplifier can do nothing, since general record equality is
@@ -284,10 +285,19 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isanewline
 \ \ \isamarkupfalse%
-\isamarkupfalse%
-\isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
+\isacommand{apply}\ {\isacharparenleft}drule{\isacharunderscore}tac\ f\ {\isacharequal}\ Xcoord\ \isakeyword{in}\ arg{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ Xcoord\ {\isacharparenleft}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isacharparenright}\ {\isacharequal}\ Xcoord\ {\isacharparenleft}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}{\isacharparenright}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}%
+\end{isabelle}
+    Now, \isa{simp} will reduce the assumption to the desired
+    conclusion.%
+\end{isamarkuptxt}%
+\ \ \isamarkuptrue%
+\isacommand{apply}\ simp\isanewline
+\ \ \isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 The \isa{cases} method is preferable to such a forward proof.  We
@@ -295,11 +305,31 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}\ {\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}{\isachardoublequote}\isamarkupfalse%
-\isamarkuptrue%
-\isamarkupfalse%
-\isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+The \methdx{cases} method adds an equality to replace the
+  named record term by an explicit record expression, listing all
+  fields.  It even includes the pseudo-field \isa{more}, since the
+  record equality stated here is generic for all extensions.%
+\end{isamarkuptxt}%
+\ \ \isamarkuptrue%
+\isacommand{apply}\ {\isacharparenleft}cases\ r{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}Xcoord\ Ycoord\ more{\isachardot}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}\ {\isacharequal}\ r{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharequal}\ a{\isacharprime}{\isasymrparr}{\isacharsemicolon}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }r\ {\isacharequal}\ {\isasymlparr}Xcoord\ {\isacharequal}\ Xcoord{\isacharcomma}\ Ycoord\ {\isacharequal}\ Ycoord{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ more{\isasymrparr}{\isasymrbrakk}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ a\ {\isacharequal}\ a{\isacharprime}%
+\end{isabelle} Again, \isa{simp} finishes the proof.  Because \isa{r} is now represented as
+  an explicit record construction, the updates can be applied and the
+  record equality can be replaced by equality of the corresponding
+  fields (due to injectivity).%
+\end{isamarkuptxt}%
+\ \ \isamarkuptrue%
+\isacommand{apply}\ simp\isanewline
+\ \ \isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 The generic cases method does not admit references to locally bound
@@ -386,10 +416,17 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}cpt{\isadigit{1}}\ {\isacharequal}\ cpt{\isadigit{2}}{\isachardoublequote}\isanewline
 \ \ \isamarkupfalse%
-\isamarkupfalse%
-\isamarkuptrue%
-\isamarkupfalse%
-\isamarkupfalse%
+\isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ cpt{\isadigit{1}}{\isacharunderscore}def\ cpt{\isadigit{2}}{\isacharunderscore}def\ point{\isachardot}defs\ cpoint{\isachardot}defs{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ Xcoord\ pt{\isadigit{1}}\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}\ {\isasymand}\ Ycoord\ pt{\isadigit{1}}\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}%
+\end{isabelle}%
+\end{isamarkuptxt}%
+\ \ \isamarkuptrue%
+\isacommand{apply}\ {\isacharparenleft}simp\ add{\isacharcolon}\ pt{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 In the example below, a coloured point is truncated to leave a
@@ -398,7 +435,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}point{\isachardot}truncate\ cpt{\isadigit{2}}\ {\isacharequal}\ pt{\isadigit{1}}{\isachardoublequote}\isanewline
 \ \ \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ pt{\isadigit{1}}{\isacharunderscore}def\ cpt{\isadigit{2}}{\isacharunderscore}def\ point{\isachardot}defs{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \begin{exercise}

--- a/doc-src/TutorialI/Types/document/Typedefs.tex	Thu Jun 09 12:04:53 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Typedefs.tex	Thu Jun 09 12:06:38 2005 +0200
@@ -87,9 +87,21 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{typedef}\ three\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+In order to enforce that the representing set on the right-hand side is
+non-empty, this definition actually starts a proof to that effect:
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymexists}x{\isachardot}\ x\ {\isasymin}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}%
+\end{isabelle}
+Fortunately, this is easy enough to show, even \isa{auto} could do it.
+In general, one has to provide a witness, in our case 0:%
+\end{isamarkuptxt}%
 \isamarkuptrue%
+\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isadigit{0}}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}\ simp\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 This type definition introduces the new type \isa{three} and asserts
@@ -188,7 +200,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymnoteq}\ B\ {\isasymand}\ B\ {\isasymnoteq}\ A\ {\isasymand}\ A\ {\isasymnoteq}\ C\ {\isasymand}\ C\ {\isasymnoteq}\ A\ {\isasymand}\ B\ {\isasymnoteq}\ C\ {\isasymand}\ C\ {\isasymnoteq}\ B{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Abs{\isacharunderscore}three{\isacharunderscore}inject\ A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def\ three{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -201,11 +213,24 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\ three{\isacharunderscore}cases{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x{\isachardoublequote}\isamarkupfalse%
-\isamarkuptrue%
-\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent Again this follows easily from a pre-proved general theorem:%
+\end{isamarkuptxt}%
 \isamarkuptrue%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ rule{\isacharcolon}\ Abs{\isacharunderscore}three{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}y{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}%
+\end{isabelle}
+Simplification with \isa{three{\isacharunderscore}def} leads to the disjunction \isa{y\ {\isacharequal}\ {\isadigit{0}}\ {\isasymor}\ y\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ y\ {\isacharequal}\ {\isadigit{2}}} which \isa{auto} separates into three
+subgoals, each of which is easily solved by simplification:%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ three{\isacharunderscore}def\ A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent

--- a/doc-src/ZF/isabelle.sty	Thu Jun 09 12:04:53 2005 +0200
+++ b/doc-src/ZF/isabelle.sty	Thu Jun 09 12:06:38 2005 +0200
@@ -3,6 +3,7 @@
 %%
 %% macros for Isabelle generated LaTeX output
 %%
+%% 
 
 %%% Simple document preparation (based on theory token language and symbols)
 
@@ -23,8 +24,15 @@
 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
+\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
+\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
+\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
+
 \newdimen\isa@parindent\newdimen\isa@parskip
 
 \newenvironment{isabellebody}{%
@@ -41,6 +49,7 @@
 
 \newcommand{\isaindent}[1]{\hphantom{#1}}
 \newcommand{\isanewline}{\mbox{}\par\mbox{}}
+\newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}}
 \newcommand{\isadigit}[1]{#1}
 
 \chardef\isacharbang=`\!

--- a/doc-src/ZF/isabellesym.sty	Thu Jun 09 12:04:53 2005 +0200
+++ b/doc-src/ZF/isabellesym.sty	Thu Jun 09 12:06:38 2005 +0200
@@ -3,19 +3,20 @@
 %%
 %% definitions of standard Isabelle symbols
 %%
+%% 
 
 % symbol definitions
 
-\newcommand{\isasymzero}{\isamath{\mathbf{0}}}  %requires amssym
-\newcommand{\isasymone}{\isamath{\mathbf{1}}}   %requires amssym
-\newcommand{\isasymtwo}{\isamath{\mathbf{2}}}   %requires amssym
-\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssym
-\newcommand{\isasymfour}{\isamath{\mathbf{4}}}  %requires amssym
-\newcommand{\isasymfive}{\isamath{\mathbf{5}}}  %requires amssym
-\newcommand{\isasymsix}{\isamath{\mathbf{6}}}   %requires amssym
-\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssym
-\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssym
-\newcommand{\isasymnine}{\isamath{\mathbf{9}}}  %requires amssym
+\newcommand{\isasymzero}{\isamath{\mathbf{0}}}  %requires amssymb
+\newcommand{\isasymone}{\isamath{\mathbf{1}}}   %requires amssymb
+\newcommand{\isasymtwo}{\isamath{\mathbf{2}}}   %requires amssymb
+\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
+\newcommand{\isasymfour}{\isamath{\mathbf{4}}}  %requires amssymb
+\newcommand{\isasymfive}{\isamath{\mathbf{5}}}  %requires amssymb
+\newcommand{\isasymsix}{\isamath{\mathbf{6}}}   %requires amssymb
+\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
+\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
+\newcommand{\isasymnine}{\isamath{\mathbf{9}}}  %requires amssymb
 \newcommand{\isasymA}{\isamath{\mathcal{A}}}
 \newcommand{\isasymB}{\isamath{\mathcal{B}}}
 \newcommand{\isasymC}{\isamath{\mathcal{C}}}
@@ -183,7 +184,12 @@
 \newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
 \newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
 \newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
-\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires amssym
+\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}}  %requires amssymb
+\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}}  %requires amssymb
+\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}}  %requires amssymb
+\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}}  %requires amssymb
+\newcommand{\isasymrestriction}{\isamath{\restriction}}  %requires amssymb
+\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires amssymb
 \newcommand{\isasymup}{\isamath{\uparrow}}
 \newcommand{\isasymUp}{\isamath{\Uparrow}}
 \newcommand{\isasymdown}{\isamath{\downarrow}}
@@ -214,8 +220,9 @@
 \newcommand{\isasymOr}{\isamath{\bigvee}}
 \newcommand{\isasymforall}{\isamath{\forall\,}}
 \newcommand{\isasymexists}{\isamath{\exists\,}}
-\newcommand{\isasymbox}{\isamath{\Box}}  %requires amssym
-\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssym
+\newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb
+\newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
+\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
 \newcommand{\isasymturnstile}{\isamath{\vdash}}
 \newcommand{\isasymTurnstile}{\isamath{\models}}
 \newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
@@ -236,8 +243,8 @@
 \newcommand{\isasymsupset}{\isamath{\supset}}
 \newcommand{\isasymsubseteq}{\isamath{\subseteq}}
 \newcommand{\isasymsupseteq}{\isamath{\supseteq}}
-\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}
-\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires amssym
+\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}  %requires amssymb
+\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires amssymb
 \newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
 \newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
 \newcommand{\isasyminter}{\isamath{\cap}}
@@ -247,7 +254,7 @@
 \newcommand{\isasymsqunion}{\isamath{\sqcup}}
 \newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
 \newcommand{\isasymsqinter}{\isamath{\sqcap}}
-\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires masmath
+\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires amsmath
 \newcommand{\isasymuplus}{\isamath{\uplus}}
 \newcommand{\isasymUplus}{\isamath{\biguplus\,}}
 \newcommand{\isasymnoteq}{\isamath{\not=}}
@@ -261,6 +268,8 @@
 \newcommand{\isasymequiv}{\isamath{\equiv}}
 \newcommand{\isasymfrown}{\isamath{\frown}}
 \newcommand{\isasympropto}{\isamath{\propto}}
+\newcommand{\isasymsome}{\isamath{\epsilon\,}}
+\newcommand{\isasymJoin}{\isamath{\Join}}  %requires amssymb
 \newcommand{\isasymbowtie}{\isamath{\bowtie}}
 \newcommand{\isasymprec}{\isamath{\prec}}
 \newcommand{\isasymsucc}{\isamath{\succ}}
@@ -278,10 +287,10 @@
 \newcommand{\isasymcirc}{\isamath{\circ}}
 \newcommand{\isasymdagger}{\isamath{\dagger}}
 \newcommand{\isasymddagger}{\isamath{\ddagger}}
-\newcommand{\isasymlhd}{\isamath{\lhd}}
-\newcommand{\isasymrhd}{\isamath{\rhd}}
-\newcommand{\isasymunlhd}{\isamath{\unlhd}}
-\newcommand{\isasymunrhd}{\isamath{\unrhd}}
+\newcommand{\isasymlhd}{\isamath{\lhd}}  %requires amssymb
+\newcommand{\isasymrhd}{\isamath{\rhd}}  %requires amssymb
+\newcommand{\isasymunlhd}{\isamath{\unlhd}}  %requires amssymb
+\newcommand{\isasymunrhd}{\isamath{\unrhd}}  %requires amssymb
 \newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
 \newcommand{\isasymtriangleright}{\isamath{\triangleright}}
 \newcommand{\isasymtriangle}{\isamath{\triangle}}
@@ -339,9 +348,8 @@
 \newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
 \newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires latin1
 \newcommand{\isasymamalg}{\isamath{\amalg}}
-\newcommand{\isasymmho}{\isamath{\mho}}  %requires amssym
-\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssym
-\newcommand{\isasymJoin}{\isamath{\Join}}  %requires amssym
+\newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb
+\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb
 \newcommand{\isasymwp}{\isamath{\wp}}
 \newcommand{\isasymwrong}{\isamath{\wr}}
 \newcommand{\isasymstruct}{\isamath{\diamond}}