# HG changeset patch
# User nipkow
# Date 967556609 -7200
# Node ID a5f86aed785b82b20ddcf9d73580fb4124690275
# Parent  7e51c9f3d5a04344ec4724097355d1fb72b07784
*** empty log message ***

diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/CodeGen/document/CodeGen.tex
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Datatype/document/ABexpr.tex
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Datatype/document/Fundata.tex
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Datatype/document/Nested.tex
--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Datatype/document/unfoldnested.tex
--- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Tue Aug 29 15:43:29 2000 +0200
@@ -97,7 +97,7 @@
 
 HOL-Misc: HOL $(LOG)/HOL-Misc.gz
 
-$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy Misc/cases.thy \
+$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \
   Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy \
   Misc/prime_def.thy Misc/case_exprs.thy \
   Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \
diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/ROOT.ML
--- a/doc-src/TutorialI/Misc/ROOT.ML	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/ROOT.ML	Tue Aug 29 15:43:29 2000 +0200
@@ -1,6 +1,5 @@
 use_thy "Tree";
 use_thy "Tree2";
-use_thy "cases";
 use_thy "case_exprs";
 use_thy "fakenat";
 use_thy "natsum";
diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/cases.thy
--- a/doc-src/TutorialI/Misc/cases.thy	Tue Aug 29 15:13:10 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(*<*)
-theory "cases" = Main:;
-(*>*)
-
-subsection{*Structural induction and case distinction*}
-
-text{*
-\indexbold{structural induction}
-\indexbold{induction!structural}
-\indexbold{case distinction}
-Almost all the basic laws about a datatype are applied automatically during
-simplification. Only induction is invoked by hand via \isaindex{induct_tac},
-which works for any datatype. In some cases, induction is overkill and a case
-distinction over all constructors of the datatype suffices. This is performed
-by \isaindexbold{case_tac}. A trivial example:
-*}
-
-lemma "(case xs of [] \\<Rightarrow> [] | y#ys \\<Rightarrow> xs) = xs";
-apply(case_tac xs);
-
-txt{*\noindent
-results in the proof state
-\begin{isabellepar}%
-~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
-~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
-\end{isabellepar}%
-which is solved automatically:
-*}
-
-by(auto)
-
-text{*
-Note that we do not need to give a lemma a name if we do not intend to refer
-to it explicitly in the future.
-*}
-
-(*<*)
-end
-(*>*)
diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/Itrev.tex
--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/Tree.tex
--- a/doc-src/TutorialI/Misc/document/Tree.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/Tree2.tex
--- a/doc-src/TutorialI/Misc/document/Tree2.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/arith1.tex
--- a/doc-src/TutorialI/Misc/document/arith1.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith1.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/arith2.tex
--- a/doc-src/TutorialI/Misc/document/arith2.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith2.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/arith3.tex
--- a/doc-src/TutorialI/Misc/document/arith3.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith3.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/arith4.tex
--- a/doc-src/TutorialI/Misc/document/arith4.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith4.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/asm_simp.tex
--- a/doc-src/TutorialI/Misc/document/asm_simp.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/asm_simp.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/case_splits.tex
--- a/doc-src/TutorialI/Misc/document/case_splits.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/case_splits.tex	Tue Aug 29 15:43:29 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
 %
 \begin{isamarkuptext}%
 Goals containing \isaindex{if}-expressions are usually proved by case
@@ -82,7 +83,7 @@
 If you need to split both in the assumptions and the conclusion,
 use $t$\isa{.splits} which subsumes $t$\isa{.split} and $t$\isa{.split_asm}.%
 \end{isamarkuptxt}%
-\end{isabelle}%
+\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/cases.tex
--- a/doc-src/TutorialI/Misc/document/cases.tex	Tue Aug 29 15:13:10 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-\begin{isabelle}%
-%
-\isamarkupsubsection{Structural induction and case distinction}
-%
-\begin{isamarkuptext}%
-\indexbold{structural induction}
-\indexbold{induction!structural}
-\indexbold{case distinction}
-Almost all the basic laws about a datatype are applied automatically during
-simplification. Only induction is invoked by hand via \isaindex{induct_tac},
-which works for any datatype. In some cases, induction is overkill and a case
-distinction over all constructors of the datatype suffices. This is performed
-by \isaindexbold{case_tac}. A trivial example:%
-\end{isamarkuptext}%
-\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}%
-\begin{isamarkuptxt}%
-\noindent
-results in the proof state
-\begin{isabellepar}%
-~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
-~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
-\end{isabellepar}%
-which is solved automatically:%
-\end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
-\begin{isamarkuptext}%
-Note that we do not need to give a lemma a name if we do not intend to refer
-to it explicitly in the future.%
-\end{isamarkuptext}%
-\end{isabelle}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/cond_rewr.tex
--- a/doc-src/TutorialI/Misc/document/cond_rewr.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/def_rewr.tex
--- a/doc-src/TutorialI/Misc/document/def_rewr.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/def_rewr.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/fakenat.tex
--- a/doc-src/TutorialI/Misc/document/fakenat.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/fakenat.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/let_rewr.tex
--- a/doc-src/TutorialI/Misc/document/let_rewr.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/let_rewr.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/pairs.tex
--- a/doc-src/TutorialI/Misc/document/pairs.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/pairs.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/prime_def.tex
--- a/doc-src/TutorialI/Misc/document/prime_def.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/trace_simp.tex
--- a/doc-src/TutorialI/Misc/document/trace_simp.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/trace_simp.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Misc/document/types.tex
--- a/doc-src/TutorialI/Misc/document/types.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex	Tue Aug 29 15:43:29 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 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Recdef/document/Induction.tex
--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Tue Aug 29 15:43:29 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
 %
 \begin{isamarkuptext}%
 Assuming we have defined our function such that Isabelle could prove
@@ -62,7 +63,7 @@
 empty list, the singleton list, and the list with at least two elements
 (in which case you may assume it holds for the tail of that list).%
 \end{isamarkuptext}%
-\end{isabelle}%
+\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Recdef/document/Nested0.tex
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex	Tue Aug 29 15:43:29 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
 %
 \begin{isamarkuptext}%
 In \S\ref{sec:nested-datatype} we defined the datatype of terms%
@@ -16,7 +17,7 @@
 
 FIXME: declare trev now!%
 \end{isamarkuptext}%
-\end{isabelle}%
+\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Recdef/document/Nested1.tex
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Tue Aug 29 15:43:29 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
 \isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
@@ -38,7 +39,7 @@
 We will now prove the termination condition and continue with our definition.
 Below we return to the question of how \isacommand{recdef} ``knows'' about \isa{map}.%
 \end{isamarkuptext}%
-\end{isabelle}%
+\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Recdef/document/Nested2.tex
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Aug 29 15:43:29 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
 %
 \begin{isamarkuptext}%
 \noindent
@@ -90,7 +91,7 @@
 declaring a congruence rule for the simplifier does not make it
 available to \isacommand{recdef}, and vice versa. This is intentional.%
 \end{isamarkuptext}%
-\end{isabelle}%
+\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Recdef/document/examples.tex
--- a/doc-src/TutorialI/Recdef/document/examples.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex	Tue Aug 29 15:43:29 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
 %
 \begin{isamarkuptext}%
 Here is a simple example, the Fibonacci function:%
@@ -77,7 +78,7 @@
 For non-recursive functions the termination measure degenerates to the empty
 set \isa{\{\}}.%
 \end{isamarkuptext}%
-\end{isabelle}%
+\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Recdef/document/simplification.tex
--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Tue Aug 29 15:43:29 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
 %
 \begin{isamarkuptext}%
 Once we have succeeded in proving all termination conditions, the recursion
@@ -100,7 +101,7 @@
 after which we can disable the original simplification rule:%
 \end{isamarkuptext}%
 \isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ gcd{\isachardot}simps\isanewline
-\end{isabelle}%
+\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Recdef/document/termination.tex
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Tue Aug 29 15:43:29 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
 %
 \begin{isamarkuptext}%
 When a function is defined via \isacommand{recdef}, Isabelle tries to prove
@@ -86,7 +87,7 @@
 For details see the manual~\cite{isabelle-HOL} and the examples in the
 library.%
 \end{isamarkuptext}%
-\end{isabelle}%
+\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/ToyList/document/ToyList.tex
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Aug 29 15:43:29 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
 \isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}%
 \begin{isamarkuptext}%
 \noindent
@@ -324,7 +325,7 @@
 we are finished with its development:%
 \end{isamarkuptext}%
 \isacommand{end}\isanewline
-\end{isabelle}%
+\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Trie/document/Option2.tex
--- a/doc-src/TutorialI/Trie/document/Option2.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Option2.tex	Tue Aug 29 15:43:29 2000 +0200
@@ -1,6 +1,7 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
 \isanewline
-\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabelle}%
+\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
diff -r 7e51c9f3d5a0 -r a5f86aed785b doc-src/TutorialI/Trie/document/Trie.tex
--- a/doc-src/TutorialI/Trie/document/Trie.tex	Tue Aug 29 15:13:10 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Tue Aug 29 15:43:29 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
 %
 \begin{isamarkuptext}%
 To minimize running time, each node of a trie should contain an array that maps
@@ -122,7 +123,7 @@
 solves the proof. Part~\ref{Isar} shows you how to write readable and stable
 proofs.%
 \end{isamarkuptext}%
-\end{isabelle}%
+\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"