# HG changeset patch # User paulson # Date 1040119541 -3600 # Node ID ee898d32de21eed63d3ef07bb9da7918cf9c1125 # Parent 33b84d172c97068b56b458bf05257cc921a4cb0a auto-update diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Advanced/document/Partial.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Advanced/document/WFrec.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Advanced/document/simp.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/CodeGen/document/CodeGen.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Datatype/document/ABexpr.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Datatype/document/Fundata.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Datatype/document/Nested.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Datatype/document/unfoldnested.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Documents/document/Documents.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Inductive/document/AB.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Inductive/document/Mutual.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Inductive/document/Star.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/AdvancedInd.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/Itrev.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/Option2.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/Plus.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/Tree.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/Tree2.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/appendix.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/case_exprs.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/fakenat.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/natsum.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/pairs.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/prime_def.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/simp.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Misc/document/types.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Recdef/document/Induction.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Recdef/document/Nested0.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Recdef/document/Nested1.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Recdef/document/Nested2.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Recdef/document/examples.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Recdef/document/simplification.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Recdef/document/termination.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Trie/document/Trie.tex --- 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: diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/Types/document/Numbers.tex --- 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}% diff -r 33b84d172c97 -r ee898d32de21 doc-src/TutorialI/isabellesym.sty --- 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