# HG changeset patch # User wenzelm # Date 967542736 -7200 # Node ID 699de91b15e2e6add0bfc5699ea96cadaa70bb32 # Parent 9be481b4bc852eab8c0edaa4f11d0412efce5483 updated; diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/CodeGen/document/CodeGen.tex --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% \noindent @@ -111,7 +112,7 @@ However, this is unnecessary because the generalized version fully subsumes its instance.% \end{isamarkuptext}% -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Datatype/document/ABexpr.tex --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% Sometimes it is necessary to define two datatypes that depend on each @@ -111,7 +112,7 @@ it. ({\em Hint:} proceed as in \S\ref{sec:boolex}). \end{exercise}% \end{isamarkuptext}% -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Datatype/document/Fundata.tex --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Branch\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}% \begin{isamarkuptext}% \noindent Parameter \isa{'a} is the type of values stored in @@ -49,7 +50,7 @@ ~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)% \end{isabellepar}%% \end{isamarkuptext}% -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Datatype/document/Nested.tex --- a/doc-src/TutorialI/Datatype/document/Nested.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% So far, all datatypes had the property that on the right-hand side of their @@ -121,7 +122,7 @@ constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of expressions as its argument: \isa{Sum "'a aexp list"}.% \end{isamarkuptext}% -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Datatype/document/unfoldnested.tex --- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,6 +1,7 @@ -\begin{isabelle}% +% +\begin{isabellebody}% \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}a\ {\isacharbar}\ App\ {\isacharprime}b\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\isanewline -\isakeyword{and}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabelle}% +\isakeyword{and}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list\ {\isacharequal}\ Nil\ {\isacharbar}\ Cons\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharunderscore}list{\isachardoublequote}\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% \subsubsection{How can we model boolean expressions?} @@ -131,7 +132,7 @@ and prove \isa{normal(norm b)}. Of course, this requires a lemma about normality of \isa{normif}:% \end{isamarkuptext}% -\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}\end{isabelle}% +\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}\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/AdvancedInd.tex --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% \noindent @@ -271,7 +272,7 @@ For example \isa{less\_induct} is the special case where \isa{r} is \isa{<} on \isa{nat}. For details see the library.% \end{isamarkuptext}% -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/Itrev.tex --- a/doc-src/TutorialI/Misc/document/Itrev.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% Function \isa{rev} has quadratic worst-case running time @@ -88,7 +89,7 @@ will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind} to learn about some advanced techniques for inductive proofs.% \end{isamarkuptxt}% -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/Tree.tex --- a/doc-src/TutorialI/Misc/document/Tree.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/Tree.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% \noindent @@ -16,7 +17,7 @@ Define a function \isa{flatten} that flattens a tree into a list by traversing it in infix order. Prove% \end{isamarkuptext}% -\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\end{isabelle}% +\isacommand{lemma}\ {\isachardoublequote}flatten{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ rev{\isacharparenleft}flatten\ t{\isacharparenright}{\isachardoublequote}\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/Tree2.tex --- a/doc-src/TutorialI/Misc/document/Tree2.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% \noindent In Exercise~\ref{ex:Tree} we defined a function @@ -11,7 +12,7 @@ \begin{isamarkuptext}% \noindent Define \isa{flatten2} and prove% \end{isamarkuptext}% -\isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabelle}% +\isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/arith1.tex --- a/doc-src/TutorialI/Misc/document/arith1.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith1.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,6 +1,7 @@ -\begin{isabelle}% +% +\begin{isabellebody}% \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/arith2.tex --- a/doc-src/TutorialI/Misc/document/arith2.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith2.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,7 +1,8 @@ -\begin{isabelle}% +% +\begin{isabellebody}% \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 \isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/arith3.tex --- a/doc-src/TutorialI/Misc/document/arith3.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith3.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,6 +1,7 @@ -\begin{isabelle}% +% +\begin{isabellebody}% \isacommand{lemma}\ {\isachardoublequote}n{\isacharasterisk}n\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ n{\isacharequal}\isadigit{0}\ {\isasymor}\ n{\isacharequal}\isadigit{1}{\isachardoublequote}\isanewline -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/arith4.tex --- a/doc-src/TutorialI/Misc/document/arith4.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith4.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,6 +1,7 @@ -\begin{isabelle}% +% +\begin{isabellebody}% \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ m\ {\isacharless}\ n\ {\isasymand}\ m\ {\isacharless}\ n{\isacharplus}\isadigit{1}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/asm_simp.tex --- a/doc-src/TutorialI/Misc/document/asm_simp.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/asm_simp.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% By default, assumptions are part of the simplification process: they are used @@ -44,7 +45,7 @@ Note that only one of the above options is allowed, and it must precede all other arguments.% \end{isamarkuptext}% -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/case_splits.tex --- a/doc-src/TutorialI/Misc/document/case_splits.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/case_splits.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% Goals containing \isaindex{if}-expressions are usually proved by case @@ -64,7 +65,7 @@ or globally:% \end{isamarkuptext}% \isacommand{lemmas}\ {\isacharbrackleft}split\ del{\isacharbrackright}\ {\isacharequal}\ list{\isachardot}split\isanewline -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/cases.tex --- a/doc-src/TutorialI/Misc/document/cases.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/cases.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% \isanewline \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ y{\isacharhash}ys\ {\isasymRightarrow}\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ xs{\isacharparenright}% @@ -12,7 +13,7 @@ which is solved automatically:% \end{isamarkuptxt}% \isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/cond_rewr.tex --- a/doc-src/TutorialI/Misc/document/cond_rewr.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% So far all examples of rewrite rules were equations. The simplifier also @@ -23,7 +24,7 @@ simplifies to \isa{xs \isasymnoteq\ []}, which is exactly the local assumption of the subgoal.% \end{isamarkuptext}% -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/def_rewr.tex --- a/doc-src/TutorialI/Misc/document/def_rewr.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/def_rewr.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% \noindent Constant definitions (\S\ref{sec:ConstDefinitions}) can @@ -38,7 +39,7 @@ You should normally not turn a definition permanently into a simplification rule because this defeats the whole purpose of an abbreviation.% \end{isamarkuptext}% -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/fakenat.tex --- a/doc-src/TutorialI/Misc/document/fakenat.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/fakenat.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,11 +1,12 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% \noindent The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural numbers is predefined and behaves like% \end{isamarkuptext}% -\isacommand{datatype}\ nat\ {\isacharequal}\ \isadigit{0}\ {\isacharbar}\ Suc\ nat\end{isabelle}% +\isacommand{datatype}\ nat\ {\isacharequal}\ \isadigit{0}\ {\isacharbar}\ Suc\ nat\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/let_rewr.tex --- a/doc-src/TutorialI/Misc/document/let_rewr.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/let_rewr.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,11 +1,12 @@ -\begin{isabelle}% +% +\begin{isabellebody}% \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}let\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ in\ xs{\isacharat}ys{\isacharat}xs{\isacharparenright}\ {\isacharequal}\ ys{\isachardoublequote}\isanewline \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptext}% If, in a particular context, there is no danger of a combinatorial explosion of nested \isa{let}s one could even add \isa{Let_def} permanently:% \end{isamarkuptext}% -\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabelle}% +\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/natsum.tex --- a/doc-src/TutorialI/Misc/document/natsum.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% \noindent @@ -22,7 +23,7 @@ \isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline \isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/pairs.tex --- a/doc-src/TutorialI/Misc/document/pairs.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/pairs.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ * @@ -20,7 +21,7 @@ \end{quote} Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).% \end{isamarkuptext}% -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/prime_def.tex --- a/doc-src/TutorialI/Misc/document/prime_def.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/prime_def.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% \isanewline \ \ \ \ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% @@ -8,7 +9,7 @@ right-hand side, which would introduce an inconsistency (why?). What you should have written is% \end{isamarkuptext}% -\ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}\end{isabelle}% +\ {\isachardoublequote}prime{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ {\isacharparenleft}m{\isacharequal}\isadigit{1}\ {\isasymor}\ m{\isacharequal}p{\isacharparenright}{\isacharparenright}{\isachardoublequote}\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/trace_simp.tex --- a/doc-src/TutorialI/Misc/document/trace_simp.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/trace_simp.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% % \begin{isamarkuptext}% Using the simplifier effectively may take a bit of experimentation. Set the @@ -36,7 +37,7 @@ of rewrite rules). Thus it is advisable to reset it:% \end{isamarkuptxt}% \isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/Misc/document/types.tex --- a/doc-src/TutorialI/Misc/document/types.tex Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/types.tex Tue Aug 29 11:52:16 2000 +0200 @@ -1,4 +1,5 @@ -\begin{isabelle}% +% +\begin{isabellebody}% \isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline \ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline \ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}% @@ -38,7 +39,7 @@ in which case the default name of each definition is \isa{$f$_def}, where $f$ is the name of the defined constant.% \end{isamarkuptext}% -\end{isabelle}% +\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 9be481b4bc85 -r 699de91b15e2 doc-src/TutorialI/isabelle.sty --- a/doc-src/TutorialI/isabelle.sty Tue Aug 29 00:57:24 2000 +0200 +++ b/doc-src/TutorialI/isabelle.sty Tue Aug 29 11:52:16 2000 +0200 @@ -16,10 +16,14 @@ \newdimen\isa@parindent\newdimen\isa@parskip -\newenvironment{isabelle}{% -\trivlist\isa@parindent\parindent\parindent0pt% +\newenvironment{isabellebody}{% +\isa@parindent\parindent\parindent0pt% \isa@parskip\parskip\parskip0pt% -\isastyle\item\relax}{\endtrivlist} +\isastyle}{} + +\newenvironment{isabelle} +{\begin{isabellebody}\begin{trivlist}\item\relax} +{\end{trivlist}\end{isabellebody}} \newcommand{\isa}[1]{\emph{\isastyleminor #1}} @@ -62,8 +66,9 @@ % keyword and section markup +\newcommand{\isakeywordcharunderscore}{\_} \newcommand{\isakeyword}[1] -{\emph{\bf\def\isachardot{.}\def\isacharunderscore{-}% +{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}% \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}} \newcommand{\isacommand}[1]{\isakeyword{#1}} @@ -90,6 +95,7 @@ \newcommand{\isabellestyleit}{% \renewcommand{\isastyle}{\small\it}% \renewcommand{\isastyleminor}{\it}% +\renewcommand{\isakeywordcharunderscore}{-}% %\renewcommand{\isadigit}[1]{\emph{$##1$}} \renewcommand{\isacharbang}{\emph{$!$}}% \renewcommand{\isachardoublequote}{}%