--- a/doc-src/TutorialI/Recdef/document/Induction.tex Tue Aug 29 11:52:47 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Aug 29 12:08:20 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 11:52:47 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Tue Aug 29 12:08:20 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 11:52:47 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Tue Aug 29 12:08:20 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 11:52:47 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Aug 29 12:08:20 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
%
\begin{isamarkuptext}%
\noindent
@@ -77,7 +78,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 11:52:47 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex Tue Aug 29 12:08:20 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 11:52:47 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Tue Aug 29 12:08:20 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 11:52:47 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Tue Aug 29 12:08:20 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 11:52:47 2000 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Aug 29 12:08:20 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 11:52:47 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Option2.tex Tue Aug 29 12:08:20 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 11:52:47 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Tue Aug 29 12:08:20 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"