--- a/doc-src/TutorialI/Advanced/document/Partial.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex Wed Jan 15 16:43:12 2003 +0100
@@ -268,7 +268,6 @@
of a partial function, you are likely to need \isa{while}.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Wed Jan 15 16:43:12 2003 +0100
@@ -125,7 +125,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
-\isanewline
{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -138,7 +137,6 @@
declarations.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Advanced/document/simp.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Advanced/document/simp.tex Wed Jan 15 16:43:12 2003 +0100
@@ -217,7 +217,6 @@
\index{simplification|)}%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed Jan 15 16:43:12 2003 +0100
@@ -96,7 +96,8 @@
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}\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequote}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -113,7 +114,6 @@
instruction sequences:%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\isacommand{lemma}\ exec{\isacharunderscore}app{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ s\ vs\ {\isacharequal}\ exec\ ys\ s\ {\isacharparenleft}exec\ xs\ s\ vs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
@@ -126,7 +126,8 @@
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}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -137,9 +138,9 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -155,7 +156,6 @@
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Wed Jan 15 16:43:12 2003 +0100
@@ -110,7 +110,8 @@
The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isacommand{apply}\ simp{\isacharunderscore}all\isamarkupfalse%
+\isacommand{apply}\ simp{\isacharunderscore}all\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -147,7 +148,6 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Wed Jan 15 16:43:12 2003 +0100
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Fundata}%
-\isanewline
\isamarkupfalse%
\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Br\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}\isamarkupfalse%
%
@@ -46,7 +45,8 @@
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
\isamarkupfalse%
-\isacommand{done}\isamarkupfalse%
+\isacommand{done}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
%
@@ -62,7 +62,6 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Wed Jan 15 16:43:12 2003 +0100
@@ -13,7 +13,6 @@
where function symbols can be applied to a list of arguments:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\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\ list{\isachardoublequote}\isamarkupfalse%
%
@@ -127,7 +126,6 @@
\isamarkupfalse%
\isamarkupfalse%
\isanewline
-\isanewline
\isamarkupfalse%
\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
@@ -161,7 +159,6 @@
expressions as its argument: \isa{Sum}~\isa{{\isachardoublequote}{\isacharprime}a\ aexp\ list{\isachardoublequote}}.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Wed Jan 15 16:43:12 2003 +0100
@@ -1,11 +1,10 @@
%
\begin{isabellebody}%
\def\isabellecontext{unfoldnested}%
-\isanewline
\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}\isamarkupfalse%
-\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%
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Documents/document/Documents.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Wed Jan 15 16:43:12 2003 +0100
@@ -126,11 +126,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
-\isanewline
\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}\isamarkupfalse%
+\ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -147,7 +147,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\isacommand{constdefs}\isanewline
\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
@@ -155,7 +154,8 @@
\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}\isamarkupfalse%
+\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -825,7 +825,6 @@
the wrong parts, especially after rearranging the theory text.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Wed Jan 15 16:43:12 2003 +0100
@@ -157,7 +157,8 @@
\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}\isamarkupfalse%
+\ \ {\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%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
@@ -187,7 +188,8 @@
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}\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}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
@@ -212,7 +214,6 @@
\index{boolean expressions example|)}%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Inductive/document/AB.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Wed Jan 15 16:43:12 2003 +0100
@@ -224,7 +224,8 @@
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}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptxt}%
@@ -240,7 +241,8 @@
\isamarkuptrue%
\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline
\ \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptxt}%
@@ -355,7 +357,6 @@
\index{grammars!defining inductively|)}%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Inductive/document/Mutual.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Wed Jan 15 16:43:12 2003 +0100
@@ -69,7 +69,6 @@
\isamarkupfalse%
\isanewline
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Inductive/document/Star.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Inductive/document/Star.tex Wed Jan 15 16:43:12 2003 +0100
@@ -103,7 +103,6 @@
transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isamarkupfalse%
@@ -211,7 +210,6 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Wed Jan 15 16:43:12 2003 +0100
@@ -63,9 +63,9 @@
result to the usual \isa{{\isasymLongrightarrow}} form:%
\end{isamarkuptxt}%
\isamarkuptrue%
-\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%
+\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%
\isamarkupfalse%
%
\begin{isamarkuptxt}%
@@ -247,7 +247,8 @@
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}\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}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -338,7 +339,6 @@
\isa{nat}. The details can be found in theory \isa{Wellfounded_Recursion}.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/Itrev.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Wed Jan 15 16:43:12 2003 +0100
@@ -91,9 +91,9 @@
just not true. The correct generalization is%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
-\isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptxt}%
@@ -119,9 +119,9 @@
for all \isa{ys} instead of a fixed one:%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
-\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}ys{\isachardot}\ itrev\ xs\ ys\ {\isacharequal}\ rev\ xs\ {\isacharat}\ ys{\isachardoublequote}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -159,7 +159,6 @@
\index{induction heuristics|)}%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/Option2.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/Option2.tex Wed Jan 15 16:43:12 2003 +0100
@@ -26,7 +26,6 @@
\S\ref{sec:Trie}.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/Plus.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/Plus.tex Wed Jan 15 16:43:12 2003 +0100
@@ -19,11 +19,10 @@
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
-\isacommand{lemma}\ {\isachardoublequote}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequote}\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isanewline
+\isamarkupfalse%
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/Tree.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/Tree.tex Wed Jan 15 16:43:12 2003 +0100
@@ -18,7 +18,8 @@
by swapping subtrees recursively. Prove%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isamarkupfalse%
+\isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
@@ -30,10 +31,10 @@
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}\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\isanewline
\isamarkupfalse%
\isamarkupfalse%
-\isanewline
+\isamarkupfalse%
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/Tree2.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex Wed Jan 15 16:43:12 2003 +0100
@@ -11,7 +11,8 @@
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}\isamarkupfalse%
+\isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -20,11 +21,10 @@
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
-\isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isanewline
+\isamarkupfalse%
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/appendix.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/appendix.tex Wed Jan 15 16:43:12 2003 +0100
@@ -34,7 +34,6 @@
\end{table}%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Wed Jan 15 16:43:12 2003 +0100
@@ -80,7 +80,8 @@
which is solved automatically:%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -103,7 +104,6 @@
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/fakenat.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/fakenat.tex Wed Jan 15 16:43:12 2003 +0100
@@ -9,8 +9,8 @@
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\isamarkupfalse%
-\isanewline
+\isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat\isanewline
+\isamarkupfalse%
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Wed Jan 15 16:43:12 2003 +0100
@@ -78,7 +78,8 @@
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}\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}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -88,7 +89,8 @@
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}\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}m\ {\isasymnoteq}\ {\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isasymLongrightarrow}\ m\ {\isacharless}\ n\ {\isasymor}\ n\ {\isacharless}\ m{\isachardoublequote}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -105,7 +107,8 @@
\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}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -113,7 +116,8 @@
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}\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}{\isadigit{0}}\ {\isasymor}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequote}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -132,7 +136,6 @@
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/pairs.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/pairs.tex Wed Jan 15 16:43:12 2003 +0100
@@ -33,7 +33,6 @@
For more information on pairs and records see Chapter~\ref{ch:more-types}.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/prime_def.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex Wed Jan 15 16:43:12 2003 +0100
@@ -22,7 +22,6 @@
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/simp.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Wed Jan 15 16:43:12 2003 +0100
@@ -217,9 +217,9 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -293,7 +293,8 @@
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}\isamarkupfalse%
+\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%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -341,7 +342,6 @@
Let us simplify a case analysis over lists:\index{*list.split (theorem)}%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ zs\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ y{\isacharhash}{\isacharparenleft}ys{\isacharat}zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
\isamarkupfalse%
@@ -362,9 +362,9 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -384,9 +384,9 @@
either locally%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -454,7 +454,8 @@
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -492,8 +493,8 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
+\isanewline
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/types.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/types.tex Wed Jan 15 16:43:12 2003 +0100
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{types}%
-\isanewline
\isamarkupfalse%
\isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline
\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
@@ -58,7 +57,6 @@
$f$ is the name of the defined constant.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/Induction.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Wed Jan 15 16:43:12 2003 +0100
@@ -76,7 +76,6 @@
holds for the tail of that list.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Wed Jan 15 16:43:12 2003 +0100
@@ -22,8 +22,8 @@
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}\isamarkupfalse%
-\isanewline
+\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%
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Wed Jan 15 16:43:12 2003 +0100
@@ -43,7 +43,6 @@
The termination condition is easily proved by induction:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Wed Jan 15 16:43:12 2003 +0100
@@ -2,11 +2,11 @@
\begin{isabellebody}%
\def\isabellecontext{Nested{\isadigit{2}}}%
\isanewline
-\isanewline
\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}\isamarkupfalse%
+\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -79,7 +79,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
-\isanewline
{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -99,7 +98,6 @@
%recdef from generating sensible termination conditions.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/examples.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Recdef/document/examples.tex Wed Jan 15 16:43:12 2003 +0100
@@ -100,8 +100,8 @@
\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%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/simplification.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Wed Jan 15 16:43:12 2003 +0100
@@ -112,8 +112,8 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline
+\isanewline
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/termination.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Wed Jan 15 16:43:12 2003 +0100
@@ -49,12 +49,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\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}\isamarkupfalse%
+{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -81,7 +81,6 @@
\isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} this would be of dubious value.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Trie/document/Trie.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Wed Jan 15 16:43:12 2003 +0100
@@ -213,7 +213,6 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Axioms.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Wed Jan 15 16:43:12 2003 +0100
@@ -290,7 +290,6 @@
worry us.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Overloading.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading.tex Wed Jan 15 16:43:12 2003 +0100
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Overloading}%
-\isanewline
\isamarkupfalse%
\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}ordrel\isanewline
\isamarkupfalse%
@@ -21,8 +20,8 @@
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}\isamarkupfalse%
-\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%
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Overloading0.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex Wed Jan 15 16:43:12 2003 +0100
@@ -49,7 +49,6 @@
To prevent such terms from even being formed requires the use of type classes.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Overloading1.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex Wed Jan 15 16:43:12 2003 +0100
@@ -81,7 +81,6 @@
we need to make lists a type of class \isa{ordrel}:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Overloading2.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex Wed Jan 15 16:43:12 2003 +0100
@@ -53,7 +53,6 @@
For technical reasons, it is not translated back upon output.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Pairs.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Types/document/Pairs.tex Wed Jan 15 16:43:12 2003 +0100
@@ -101,7 +101,6 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ split{\isacharunderscore}split{\isacharparenright}\isamarkupfalse%
%
@@ -121,7 +120,6 @@
can be split as above. The same is true for paired set comprehension:%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isanewline
\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%
@@ -137,7 +135,6 @@
The same proof procedure works for%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isanewline
\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%
%
@@ -150,7 +147,6 @@
may be present in the goal. Consider the following function:%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\isacommand{consts}\ swap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isachardoublequote}\isanewline
\isamarkupfalse%
@@ -192,7 +188,6 @@
with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:%
\end{isamarkuptxt}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}p\ q{\isachardot}\ swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ q\ {\isasymlongrightarrow}\ p\ {\isacharequal}\ q{\isachardoublequote}\isanewline
\isamarkupfalse%
@@ -222,9 +217,9 @@
where two separate \isa{simp} applications succeed.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isanewline
+\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -251,7 +246,6 @@
\end{center}%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Records.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Types/document/Records.tex Wed Jan 15 16:43:12 2003 +0100
@@ -452,7 +452,6 @@
\index{records|)}%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Typedefs.tex Thu Jan 09 11:45:40 2003 +0100
+++ b/doc-src/TutorialI/Types/document/Typedefs.tex Wed Jan 15 16:43:12 2003 +0100
@@ -271,7 +271,6 @@
\index{types!defining|)}%
\end{isamarkuptext}%
\isamarkuptrue%
-\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables: