--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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}{}%