# HG changeset patch
# User wenzelm
# Date 967543700 -7200
# Node ID c753196599f90838a2c4d0b813f42e139dec1b69
# Parent  d5509912af187adfc436d16fc0f922e37c1f213f
updated;

diff -r d5509912af18 -r c753196599f9 doc-src/TutorialI/Recdef/document/Induction.tex
--- 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"
diff -r d5509912af18 -r c753196599f9 doc-src/TutorialI/Recdef/document/Nested0.tex
--- 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"
diff -r d5509912af18 -r c753196599f9 doc-src/TutorialI/Recdef/document/Nested1.tex
--- 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"
diff -r d5509912af18 -r c753196599f9 doc-src/TutorialI/Recdef/document/Nested2.tex
--- 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"
diff -r d5509912af18 -r c753196599f9 doc-src/TutorialI/Recdef/document/examples.tex
--- 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"
diff -r d5509912af18 -r c753196599f9 doc-src/TutorialI/Recdef/document/simplification.tex
--- 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"
diff -r d5509912af18 -r c753196599f9 doc-src/TutorialI/Recdef/document/termination.tex
--- 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"
diff -r d5509912af18 -r c753196599f9 doc-src/TutorialI/ToyList/document/ToyList.tex
--- 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"
diff -r d5509912af18 -r c753196599f9 doc-src/TutorialI/Trie/document/Option2.tex
--- 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"
diff -r d5509912af18 -r c753196599f9 doc-src/TutorialI/Trie/document/Trie.tex
--- 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"