*** empty log message ***

--- a/doc-src/TutorialI/CTL/document/Base.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -98,7 +98,6 @@
 telling us which atomic propositions are true in each state.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isanewline
 \isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:

--- a/doc-src/TutorialI/CTL/document/CTL.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -16,7 +16,6 @@
 \isa{formula} by a new constructor%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isanewline
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula\isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -40,7 +39,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
-\isanewline
 {\isachardoublequote}s\ {\isasymTurnstile}\ AF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -59,7 +57,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
-\isanewline
 {\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -483,7 +480,6 @@
 \index{CTL|)}%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isanewline
 \isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:

--- a/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -181,7 +181,6 @@
 \isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isanewline
 \isanewline
 \isamarkupfalse%
-\isanewline
 \isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:

--- a/doc-src/TutorialI/CTL/document/PDL.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -253,7 +253,6 @@
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
-\isanewline
 \isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:

--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -96,8 +96,7 @@
 execution of a compiled expression results in the value of the expression:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{theorem}\ {\isachardoublequote}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -126,8 +125,7 @@
 automatic case splitting, which finishes the proof:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isanewline
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -139,8 +137,7 @@
 \isamarkuptrue%
 \isamarkupfalse%
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isanewline
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -110,8 +110,7 @@
 The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isacommand{apply}\ simp{\isacharunderscore}all\isanewline
-\isamarkupfalse%
+\isacommand{apply}\ simp{\isacharunderscore}all\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -45,8 +45,7 @@
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
 \isamarkupfalse%
-\isacommand{done}\isanewline
-\isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 %

--- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -3,8 +3,7 @@
 \def\isabellecontext{unfoldnested}%
 \isamarkupfalse%
 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}v\ {\isacharbar}\ App\ {\isacharprime}f\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isanewline
-\isakeyword{and}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isakeyword{and}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:

--- a/doc-src/TutorialI/Documents/document/Documents.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -129,8 +129,7 @@
 \isamarkupfalse%
 \isacommand{constdefs}\isanewline
 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -154,8 +153,7 @@
 \isanewline
 \isamarkupfalse%
 \isacommand{syntax}\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline
-\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
-\isamarkupfalse%
+\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -157,8 +157,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
@@ -188,8 +187,7 @@
 normality of \isa{normif}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%

--- a/doc-src/TutorialI/Inductive/document/AB.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -224,8 +224,7 @@
 of \isa{w}, using the induction rule \isa{length{\isacharunderscore}induct}:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isanewline
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptxt}%
@@ -241,8 +240,7 @@
 \isamarkuptrue%
 \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
 \ \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}\isanewline
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptxt}%

--- a/doc-src/TutorialI/Inductive/document/Mutual.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Inductive/document/Mutual.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -67,7 +67,6 @@
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
-\isanewline
 \isamarkupfalse%
 \isamarkupfalse%
 \end{isabellebody}%

--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -64,8 +64,7 @@
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isamarkupfalse%
-\isacommand{lemma}\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{lemma}\ hd{\isacharunderscore}rev\ {\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ last\ xs{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptxt}%
@@ -247,8 +246,7 @@
 We could have included this derivation in the original statement of the lemma:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -92,8 +92,7 @@
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isamarkupfalse%
-\isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptxt}%
@@ -120,8 +119,7 @@
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isamarkupfalse%
-\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/Misc/document/Plus.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/Plus.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -20,8 +20,7 @@
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
-\isacommand{lemma}\ {\isachardoublequote}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \end{isabellebody}%

--- a/doc-src/TutorialI/Misc/document/Tree.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/Tree.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -18,8 +18,7 @@
 by swapping subtrees recursively. Prove%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
@@ -31,8 +30,7 @@
 by traversing it in infix order. Prove%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%

--- a/doc-src/TutorialI/Misc/document/Tree2.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -11,8 +11,7 @@
 argument, the accumulator:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -22,8 +21,7 @@
 \isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
-\isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 \isamarkupfalse%
 \end{isabellebody}%

--- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -80,8 +80,7 @@
 which is solved automatically:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/Misc/document/fakenat.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/fakenat.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -9,8 +9,7 @@
 numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}.  It  behaves as if it were declared like this:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat\isanewline
-\isamarkupfalse%
+\isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat\isamarkupfalse%
 \isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:

--- a/doc-src/TutorialI/Misc/document/natsum.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -78,8 +78,7 @@
 simple arithmetic goals automatically:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isacharplus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isacharplus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -89,8 +88,7 @@
 In consequence, \isa{auto} and \isa{simp} cannot prove this slightly more complex goal:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}m\ {\isasymnoteq}\ {\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharless}\ n\ {\isasymor}\ n\ {\isacharless}\ m{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}m\ {\isasymnoteq}\ {\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharless}\ n\ {\isasymor}\ n\ {\isacharless}\ m{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -107,8 +105,7 @@
 \isamarkuptrue%
 \isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -116,8 +113,7 @@
 succeeds because \isa{k\ {\isacharasterisk}\ k} can be treated as atomic. In contrast,%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/Misc/document/simp.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -218,8 +218,7 @@
 \isamarkuptrue%
 \isamarkupfalse%
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isanewline
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -293,8 +292,7 @@
 the lemma below is proved by plain simplification:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -363,8 +361,7 @@
 \isamarkuptrue%
 \isamarkupfalse%
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}\isanewline
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -385,8 +382,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}\isanewline
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -454,8 +450,7 @@
 \isamarkupfalse%
 \isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%
@@ -493,7 +488,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
-\isanewline
 \isamarkupfalse%
 \isamarkupfalse%
 \end{isabellebody}%

--- a/doc-src/TutorialI/Recdef/document/Nested0.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -22,8 +22,7 @@
 choose exercise~\ref{ex:trev-trev}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:

--- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -5,8 +5,7 @@
 \isamarkupfalse%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}\isanewline
-\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/Recdef/document/examples.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Recdef/document/examples.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -100,7 +100,6 @@
 \isacommand{recdef}\ swap{\isadigit{1}}{\isadigit{2}}\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline
 \ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequote}\isanewline
 \ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequote}\isanewline
-\isanewline
 \isamarkupfalse%
 \isamarkupfalse%
 \end{isabellebody}%

--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -112,7 +112,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline
-\isanewline
 \isamarkupfalse%
 \isamarkupfalse%
 \end{isabellebody}%

--- a/doc-src/TutorialI/Recdef/document/termination.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -53,8 +53,7 @@
 \isacommand{recdef}\ qs\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
 \ {\isachardoublequote}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
 \ {\isachardoublequote}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequote}\isanewline
-{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}\isanewline
-\isamarkupfalse%
+{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/Rules/rules.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -758,7 +758,7 @@
 resulting subgoal is trivial by assumption, so the \isacommand{by} command
 proves it implicitly. 
 
-We are using the \isa{erule} method it in a novel way. Hitherto, 
+We are using the \isa{erule} method in a novel way. Hitherto, 
 the conclusion of the rule was just a variable such as~\isa{?R}, but it may
 be any term. The conclusion is unified with the subgoal just as 
 it would be with the \isa{rule} method. At the same time \isa{erule} looks 
@@ -1425,7 +1425,7 @@
 \[ \infer{P[(\varepsilon x. P) / \, x]}{\exists x.\,P} \]
 This rule is seldom used for that purpose --- it can cause exponential
 blow-up --- but it is occasionally used as an introduction rule
-for~$\varepsilon$-operator.  Its name in HOL is \tdxbold{someI_ex}.%%
+for the~$\varepsilon$-operator.  Its name in HOL is \tdxbold{someI_ex}.%%
 \index{description operators|)}
 
 

--- a/doc-src/TutorialI/Types/document/Overloading.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -20,8 +20,7 @@
 prefix{\isacharunderscore}def{\isacharcolon}\isanewline
 \ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ {\isasymequiv}\ \ {\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
 strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline
-\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequote}\isanewline
-\isamarkupfalse%
+\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequote}\isamarkupfalse%
 \isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:

--- a/doc-src/TutorialI/Types/document/Pairs.tex	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/Types/document/Pairs.tex	Wed Jan 29 16:29:38 2003 +0100
@@ -218,8 +218,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isanewline
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
 \isamarkupfalse%
 %
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/tutorial.ind	Wed Jan 29 11:02:08 2003 +0100
+++ b/doc-src/TutorialI/tutorial.ind	Wed Jan 29 16:29:38 2003 +0100
@@ -27,10 +27,11 @@
   \item \texttt {\%}, \bold{209}
   \item \texttt {;}, \bold{7}
   \item \isa {()} (constant), 24
+  \item * trace_unify_fail (flag), 76
   \item \isa {+} (tactical), 99
   \item \isa {<*lex*>}, \see{lexicographic product}{1}
-  \item \isa {?} (tactical), 99
-  \item \texttt{|} (tactical), 99
+  \item \isa {?} (tactical), 100
+  \item \texttt{|} (tactical), 100
 
   \indexspace
 
@@ -66,16 +67,16 @@
   \item \isa {assumption} (method), 69
   \item assumptions
     \subitem of subgoal, 12
-    \subitem renaming, 82--83
-    \subitem reusing, 83
+    \subitem renaming, 83
+    \subitem reusing, 83--84
   \item \isa {auto} (method), 38, 92
-  \item \isa {axclass}, 164--170
-  \item axiom of choice, 86
-  \item axiomatic type classes, 164--170
+  \item \isa {axclass}, 164--171
+  \item axiom of choice, 87
+  \item axiomatic type classes, 164--171
 
   \indexspace
 
-  \item \isacommand {back} (command), 78
+  \item \isacommand {back} (command), 79
   \item \isa {Ball} (constant), 109
   \item \isa {ballI} (theorem), \bold{108}
   \item \isa {best} (method), 92
@@ -87,7 +88,7 @@
   \item binary trees, 18
   \item binomial coefficients, 109
   \item bisimulations, 116
-  \item \isa {blast} (method), 89--90, 92
+  \item \isa {blast} (method), 89--92
   \item \isa {bool} (type), 4, 5
   \item boolean expressions example, 20--22
   \item \isa {bspec} (theorem), \bold{108}
@@ -103,7 +104,7 @@
   \item \isa {case} expressions, 5, 6, 18
   \item case distinctions, 19
   \item case splits, \bold{31}
-  \item \isa {case_tac} (method), 19, 101, 157
+  \item \isa {case_tac} (method), 19, 102, 158
   \item \isa {cases} (method), 162
   \item \isacommand {chapter} (command), 59
   \item \isa {clarify} (method), 91, 92
@@ -142,7 +143,7 @@
     \subitem and nested recursion, 40, 44
     \subitem mutually recursive, 38
     \subitem nested, 180
-  \item \isacommand {defer} (command), 16, 100
+  \item \isacommand {defer} (command), 16, 101
   \item Definitional Approach, 26
   \item definitions, \bold{25}
     \subitem unfolding, \bold{30}
@@ -152,7 +153,7 @@
   \item descriptions
     \subitem definite, 85
     \subitem indefinite, 86
-  \item \isa {dest} (attribute), 102
+  \item \isa {dest} (attribute), 103
   \item destruction rules, 71
   \item \isa {diff_mult_distrib} (theorem), \bold{151}
   \item difference
@@ -160,7 +161,7 @@
   \item \isa {disjCI} (theorem), \bold{74}
   \item \isa {disjE} (theorem), \bold{70}
   \item \isa {div} (symbol), 23
-  \item divides relation, 84, 95, 101--104, 152
+  \item divides relation, 84, 95, 102--104, 152
   \item division
     \subitem by negative numbers, 153
     \subitem by zero, 152
@@ -189,7 +190,7 @@
   \item \isa {equalityI} (theorem), \bold{106}
   \item \isa {erule} (method), 70
   \item \isa {erule_tac} (method), 76
-  \item Euclid's algorithm, 101--104
+  \item Euclid's algorithm, 102--104
   \item even numbers
     \subitem defining inductively, 127--131
   \item \texttt {EX}, \bold{209}
@@ -213,14 +214,14 @@
   \item \isa {finite} (symbol), 109
   \item \isa {Finites} (constant), 109
   \item fixed points, 116
-  \item flags, 5, 6, 33
+  \item flags, 5, 6, 33, 76
     \subitem setting and resetting, 5
   \item \isa {force} (method), 91, 92
   \item formal comments, \bold{61}
   \item formal proof documents, \bold{57}
   \item formulae, 5--6
-  \item forward proof, 92--98
-  \item \isa {frule} (method), 83
+  \item forward proof, 93--99
+  \item \isa {frule} (method), 83--84
   \item \isa {frule_tac} (method), 76
   \item \isa {fst} (constant), 24
   \item function types, 5
@@ -231,9 +232,9 @@
 
   \indexspace
 
-  \item \isa {gcd} (constant), 93--94, 101--104
+  \item \isa {gcd} (constant), 93--95, 102--104
   \item generalizing for induction, 129
-  \item generalizing induction formulae, 35
+  \item generalizing induction formulae, 34
   \item Girard, Jean-Yves, \fnote{71}
   \item Gordon, Mike, 3
   \item grammars
@@ -260,9 +261,9 @@
   \item identity relation, \bold{112}
   \item \isa {if} expressions, 5, 6
     \subitem simplification of, 33
-    \subitem splitting of, 31, 50
+    \subitem splitting of, 31, 49
   \item if-and-only-if, 6
-  \item \isa {iff} (attribute), 90, 102, 130
+  \item \isa {iff} (attribute), 90, 91, 103, 130
   \item \isa {iffD1} (theorem), \bold{94}
   \item \isa {iffD2} (theorem), \bold{94}
   \item ignored material, \bold{64}
@@ -282,7 +283,7 @@
     \subitem recursion, 51--52
     \subitem structural, 19
     \subitem well-founded, 115
-  \item induction heuristics, 34--36
+  \item induction heuristics, 33--35
   \item \isacommand {inductive} (command), 127
   \item inductive definition
     \subitem simultaneous, 141
@@ -294,7 +295,7 @@
   \item \isa {inj_on_def} (theorem), \bold{110}
   \item injections, 110
   \item \isa {insert} (constant), 107
-  \item \isa {insert} (method), 97--98
+  \item \isa {insert} (method), 97--99
   \item instance, \bold{166}
   \item \texttt {INT}, \bold{209}
   \item \texttt {Int}, \bold{209}
@@ -330,12 +331,12 @@
   \indexspace
 
   \item $\lambda$ expressions, 5
-  \item LCF, 44
-  \item \isa {LEAST} (symbol), 23, 85
-  \item least number operator, \see{\protect\isa{LEAST}}{85}
+  \item LCF, 43
+  \item \isa {LEAST} (symbol), 23, 86
+  \item least number operator, \see{\protect\isa{LEAST}}{86}
   \item Leibniz, Gottfried Wilhelm, 53
   \item \isacommand {lemma} (command), 13
-  \item \isacommand {lemmas} (command), 93, 102
+  \item \isacommand {lemmas} (command), 93, 103
   \item \isa {length} (symbol), 18
   \item \isa {length_induct}, \bold{190}
   \item \isa {less_than} (constant), 114
@@ -376,10 +377,10 @@
   \item \isa {mono_def} (theorem), \bold{116}
   \item monotone functions, \bold{116}, 139
     \subitem and inductive definitions, 137--138
-  \item \isa {more} (constant), 158, 160
+  \item \isa {more} (constant), 159, 160
   \item \isa {mp} (theorem), \bold{72}
   \item \isa {mult_ac} (theorems), 152
-  \item multiple inheritance, \bold{169}
+  \item multiple inheritance, \bold{170}
   \item multiset ordering, \bold{115}
 
   \indexspace
@@ -423,12 +424,12 @@
   \item pairs and tuples, 24, 155--158
   \item parent theories, \bold{4}
   \item pattern matching
-    \subitem and \isacommand{recdef}, 48
+    \subitem and \isacommand{recdef}, 47
   \item patterns
     \subitem higher-order, \bold{177}
   \item PDL, 118--120
   \item \isacommand {pr} (command), 16, 100
-  \item \isacommand {prefer} (command), 16, 100
+  \item \isacommand {prefer} (command), 16, 101
   \item prefix annotation, 55
   \item primitive recursion, \see{recursion, primitive}{1}
   \item \isacommand {primrec} (command), 10, 18, 38--44
@@ -438,7 +439,7 @@
   \item proof state, 12
   \item proofs
     \subitem abandoning, \bold{13}
-    \subitem examples of failing, 87--89
+    \subitem examples of failing, 88--89
   \item protocols
     \subitem security, 195--205
 
@@ -446,10 +447,10 @@
 
   \item quantifiers, 6
     \subitem and inductive definitions, 135--137
-    \subitem existential, 82
+    \subitem existential, 82--83
     \subitem for sets, 108
     \subitem instantiating, 84
-    \subitem universal, 79--82
+    \subitem universal, 80--82
 
   \indexspace
 
@@ -483,12 +484,11 @@
   \item \isa {rel_comp_def} (theorem), \bold{112}
   \item relations, 111--114
     \subitem well-founded, 114--115
-  \item \isa {rename_tac} (method), 82--83
+  \item \isa {rename_tac} (method), 83
   \item \isa {rev} (constant), 10--14, 34
   \item rewrite rules, \bold{27}
     \subitem permutative, \bold{176}
   \item rewriting, \bold{27}
-  \item \isa {rotate_tac} (method), 30
   \item \isa {rtrancl_refl} (theorem), \bold{112}
   \item \isa {rtrancl_trans} (theorem), \bold{112}
   \item rule induction, 128--130
@@ -526,19 +526,19 @@
   \item simplification rule, 177--178
   \item simplification rules, 28
     \subitem adding and deleting, 29
-  \item \isa {simplified} (attribute), 93, 96
+  \item \isa {simplified} (attribute), 94, 96
   \item \isa {size} (constant), 17
   \item \isa {snd} (constant), 24
   \item \isa {SOME} (symbol), 86
   \item \texttt {SOME}, \bold{209}
   \item \isa {Some} (constant), \bold{24}
-  \item \isa {some_equality} (theorem), \bold{86}
-  \item \isa {someI} (theorem), \bold{86}
-  \item \isa {someI2} (theorem), \bold{86}
+  \item \isa {some_equality} (theorem), \bold{87}
+  \item \isa {someI} (theorem), \bold{87}
+  \item \isa {someI2} (theorem), \bold{87}
   \item \isa {someI_ex} (theorem), \bold{87}
   \item sorts, 170
   \item source comments, \bold{60}
-  \item \isa {spec} (theorem), \bold{80}
+  \item \isa {spec} (theorem), \bold{81}
   \item \isa {split} (attribute), 32
   \item \isa {split} (constant), 156
   \item \isa {split} (method), 31, 156
@@ -548,9 +548,9 @@
   \item \isa {split_if_asm} (theorem), 32
   \item \isa {ssubst} (theorem), \bold{77}
   \item structural induction, \see{induction, structural}{1}
-  \item subclasses, 164, 169
+  \item subclasses, 165, 169
   \item subgoal numbering, 46
-  \item \isa {subgoal_tac} (method), 98
+  \item \isa {subgoal_tac} (method), 98, 99
   \item subgoals, 12
   \item \isacommand {subsect} (command), 59
   \item \isacommand {subsection} (command), 59
@@ -558,7 +558,7 @@
   \item \isa {subsetD} (theorem), \bold{106}
   \item \isa {subsetI} (theorem), \bold{106}
   \item \isa {subst} (method), 77
-  \item substitution, 77--79
+  \item substitution, 77--80
   \item \isacommand {subsubsect} (command), 59
   \item \isacommand {subsubsection} (command), 59
   \item \isa {Suc} (constant), 22
@@ -573,7 +573,7 @@
 
   \indexspace
 
-  \item tacticals, 99
+  \item tacticals, 99--100
   \item tactics, 12
   \item \isacommand {term} (command), 16
   \item term rewriting, \bold{27}
@@ -582,8 +582,8 @@
   \item text, \bold{61}
   \item text blocks, \bold{61}
   \item \isa {THE} (symbol), 85
-  \item \isa {the_equality} (theorem), \bold{85}
-  \item \isa {THEN} (attribute), \bold{94}, 96, 102
+  \item \isa {the_equality} (theorem), \bold{86}
+  \item \isa {THEN} (attribute), \bold{94}, 96, 103
   \item \isacommand {theorem} (command), \bold{11}, 13
   \item theories, 4
     \subitem abandoning, \bold{16}
@@ -597,7 +597,7 @@
   \item \isa {trancl_trans} (theorem), \bold{113}
   \item transition systems, 117
   \item \isacommand {translations} (command), 56
-  \item tries, 44--47
+  \item tries, 44--46
   \item \isa {True} (constant), 5
   \item \isa {truncate} (constant), 163
   \item tuples, \see{pairs and tuples}{1}
@@ -609,10 +609,10 @@
   \item type synonyms, 25
   \item type variables, 5
   \item \isacommand {typedecl} (command), 117, 171
-  \item \isacommand {typedef} (command), 171--174
+  \item \isacommand {typedef} (command), 172--174
   \item types, 4--5
     \subitem declaring, 171
-    \subitem defining, 171--174
+    \subitem defining, 172--174
   \item \isacommand {types} (command), 25
 
   \indexspace
@@ -625,7 +625,7 @@
   \item \isa {UN_iff} (theorem), \bold{108}
   \item \isa {Un_subset_iff} (theorem), \bold{106}
   \item \isacommand {undo} (command), 16
-  \item \isa {unfold} (method), \bold{31}
+  \item \isa {unfold} (method), \bold{30}
   \item unification, 76--79
   \item \isa {UNION} (constant), 109
   \item \texttt {Union}, \bold{209}