--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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 \
--- 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";
--- 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
-(*>*)
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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:
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"