--- a/doc-src/TutorialI/Advanced/document/Partial.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex Tue Dec 17 11:05:41 2002 +0100
@@ -268,6 +268,7 @@
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 Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Tue Dec 17 11:05:41 2002 +0100
@@ -125,6 +125,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
+\isanewline
{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -137,6 +138,7 @@
declarations.%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Advanced/document/simp.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Advanced/document/simp.tex Tue Dec 17 11:05:41 2002 +0100
@@ -217,6 +217,7 @@
\index{simplification|)}%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Tue Dec 17 11:05:41 2002 +0100
@@ -113,6 +113,7 @@
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%
@@ -136,6 +137,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse%
\isamarkupfalse%
@@ -153,6 +155,7 @@
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Tue Dec 17 11:05:41 2002 +0100
@@ -147,6 +147,7 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Dec 17 11:05:41 2002 +0100
@@ -1,6 +1,7 @@
%
\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%
%
@@ -61,6 +62,7 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Tue Dec 17 11:05:41 2002 +0100
@@ -13,6 +13,7 @@
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%
%
@@ -126,6 +127,7 @@
\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%
@@ -159,6 +161,7 @@
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 Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Tue Dec 17 11:05:41 2002 +0100
@@ -1,9 +1,11 @@
%
\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
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Documents/document/Documents.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Tue Dec 17 11:05:41 2002 +0100
@@ -126,6 +126,7 @@
\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
@@ -146,6 +147,7 @@
\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
@@ -823,6 +825,7 @@
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 Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Tue Dec 17 11:05:41 2002 +0100
@@ -212,6 +212,7 @@
\index{boolean expressions example|)}%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Inductive/document/AB.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Tue Dec 17 11:05:41 2002 +0100
@@ -355,6 +355,7 @@
\index{grammars!defining inductively|)}%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Inductive/document/Mutual.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Tue Dec 17 11:05:41 2002 +0100
@@ -67,7 +67,9 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Inductive/document/Star.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Inductive/document/Star.tex Tue Dec 17 11:05:41 2002 +0100
@@ -103,6 +103,7 @@
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%
@@ -210,6 +211,7 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Dec 17 11:05:41 2002 +0100
@@ -63,6 +63,7 @@
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%
\isamarkupfalse%
@@ -337,6 +338,7 @@
\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 Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Tue Dec 17 11:05:41 2002 +0100
@@ -91,6 +91,7 @@
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%
\isamarkupfalse%
@@ -118,6 +119,7 @@
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%
\isamarkupfalse%
@@ -157,6 +159,7 @@
\index{induction heuristics|)}%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/Option2.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/Option2.tex Tue Dec 17 11:05:41 2002 +0100
@@ -26,6 +26,7 @@
\S\ref{sec:Trie}.%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/Plus.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/Plus.tex Tue Dec 17 11:05:41 2002 +0100
@@ -19,9 +19,11 @@
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequote}\isamarkupfalse%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/Tree.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/Tree.tex Tue Dec 17 11:05:41 2002 +0100
@@ -33,6 +33,7 @@
\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/Tree2.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex Tue Dec 17 11:05:41 2002 +0100
@@ -20,9 +20,11 @@
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\isamarkupfalse%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/appendix.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/appendix.tex Tue Dec 17 11:05:41 2002 +0100
@@ -34,6 +34,7 @@
\end{table}%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Tue Dec 17 11:05:41 2002 +0100
@@ -103,6 +103,7 @@
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/fakenat.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/fakenat.tex Tue Dec 17 11:05:41 2002 +0100
@@ -10,6 +10,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\ nat\ {\isacharequal}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ nat\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/natsum.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Tue Dec 17 11:05:41 2002 +0100
@@ -132,6 +132,7 @@
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/pairs.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/pairs.tex Tue Dec 17 11:05:41 2002 +0100
@@ -33,6 +33,7 @@
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 Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex Tue Dec 17 11:05:41 2002 +0100
@@ -22,6 +22,7 @@
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/simp.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Tue Dec 17 11:05:41 2002 +0100
@@ -217,6 +217,7 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
\isamarkupfalse%
@@ -340,6 +341,7 @@
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%
@@ -360,6 +362,7 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}\isamarkupfalse%
\isamarkupfalse%
@@ -381,6 +384,7 @@
either locally%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}\isamarkupfalse%
\isamarkupfalse%
@@ -489,6 +493,7 @@
\isamarkuptrue%
\isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Misc/document/types.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/types.tex Tue Dec 17 11:05:41 2002 +0100
@@ -1,6 +1,7 @@
%
\begin{isabellebody}%
\def\isabellecontext{types}%
+\isanewline
\isamarkupfalse%
\isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline
\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
@@ -57,6 +58,7 @@
$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 Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Dec 17 11:05:41 2002 +0100
@@ -76,6 +76,7 @@
holds for the tail of that list.%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Tue Dec 17 11:05:41 2002 +0100
@@ -23,6 +23,7 @@
\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
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Tue Dec 17 11:05:41 2002 +0100
@@ -43,6 +43,7 @@
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 Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Dec 17 11:05:41 2002 +0100
@@ -2,6 +2,7 @@
\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%
@@ -78,6 +79,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
+\isanewline
{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -97,6 +99,7 @@
%recdef from generating sensible termination conditions.%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/examples.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Recdef/document/examples.tex Tue Dec 17 11:05:41 2002 +0100
@@ -101,6 +101,7 @@
\ \ {\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
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/simplification.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Tue Dec 17 11:05:41 2002 +0100
@@ -113,6 +113,7 @@
\isamarkuptrue%
\isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Recdef/document/termination.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Tue Dec 17 11:05:41 2002 +0100
@@ -49,6 +49,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\isacommand{recdef}\ qs\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
\ {\isachardoublequote}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
@@ -80,6 +81,7 @@
\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 Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Tue Dec 17 11:05:41 2002 +0100
@@ -213,6 +213,7 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Numbers.tex Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Tue Dec 17 11:05:41 2002 +0100
@@ -218,8 +218,11 @@
\rulename{dvd_add}
For the integers, I'd list a few theorems that somehow involve negative
-numbers.
-
+numbers.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
Division, remainder of negatives
@@ -289,6 +292,31 @@
\isacommand{by}\ {\isacharparenleft}simp\ add{\isacharcolon}\ zabs{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
+Induction rules for the Integers
+
+\begin{isabelle}%
+{\isasymlbrakk}k\ {\isasymle}\ i{\isacharsemicolon}\ P\ k{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}k\ {\isasymle}\ i{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i%
+\end{isabelle}
+\rulename{int_ge_induct}
+
+\begin{isabelle}%
+{\isasymlbrakk}k\ {\isacharless}\ i{\isacharsemicolon}\ P\ {\isacharparenleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}k\ {\isacharless}\ i{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i%
+\end{isabelle}
+\rulename{int_gr_induct}
+
+\begin{isabelle}%
+{\isasymlbrakk}i\ {\isasymle}\ k{\isacharsemicolon}\ P\ k{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}i\ {\isasymle}\ k{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i%
+\end{isabelle}
+\rulename{int_le_induct}
+
+\begin{isabelle}%
+{\isasymlbrakk}i\ {\isacharless}\ k{\isacharsemicolon}\ P\ {\isacharparenleft}k\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}i\ {\isacharless}\ k{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i%
+\end{isabelle}
+\rulename{int_less_induct}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
REALS
\begin{isabelle}%
--- a/doc-src/TutorialI/isabellesym.sty Tue Dec 17 11:04:58 2002 +0100
+++ b/doc-src/TutorialI/isabellesym.sty Tue Dec 17 11:05:41 2002 +0100
@@ -336,8 +336,8 @@
\newcommand{\isasymeuro}{\isatext{\EUR}} %requires marvosym
\newcommand{\isasympounds}{\isamath{\pounds}}
\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
-\newcommand{\isasymcent}{\isatext{\cent}} %requires wasysym
-\newcommand{\isasymcurrency}{\isatext{\currency}} %requires wasysym
+\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
+\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
\newcommand{\isasymamalg}{\isamath{\amalg}}
\newcommand{\isasymmho}{\isamath{\mho}} %requires latexsym