diff -r a5f86aed785b -r a977245dfc8a doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Aug 29 15:43:29 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Aug 29 16:05:13 2000 +0200
@@ -27,13 +27,13 @@
 Induction variable occurs also among premises!
 \end{quote}
 and leads to the base case
-\begin{isabellepar}%
+\begin{isabelle}
 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
-\end{isabellepar}%
+\end{isabelle}
 which, after simplification, becomes
-\begin{isabellepar}%
+\begin{isabelle}
 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ []
-\end{isabellepar}%
+\end{isabelle}
 We cannot prove this equality because we do not know what \isa{hd} and
 \isa{last} return when applied to \isa{[]}.
 
@@ -51,9 +51,9 @@
 \begin{isamarkuptext}%
 \noindent
 This time, induction leaves us with the following base case
-\begin{isabellepar}%
+\begin{isabelle}
 \ 1.\ []\ {\isasymnoteq}\ []\ {\isasymlongrightarrow}\ hd\ (rev\ [])\ =\ last\ []
-\end{isabellepar}%
+\end{isabelle}
 which is trivial, and \isa{auto} finishes the whole proof.
 
 If \isa{hd\_rev} is meant to be a simplification rule, you are done. But if you
@@ -151,18 +151,18 @@
 \begin{isamarkuptxt}%
 \noindent
 which leaves us with the following proof state:
-\begin{isabellepar}%
+\begin{isabelle}
 \ 1.\ {\isasymAnd}\mbox{n}.\ {\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i})\isanewline
 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymforall}\mbox{i}.\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
-\end{isabellepar}%
+\end{isabelle}
 After stripping the \isa{\isasymforall i}, the proof continues with a case
 distinction on \isa{i}. The case \isa{i = 0} is trivial and we focus on the
 other case:
-\begin{isabellepar}%
+\begin{isabelle}
 \ 1.\ {\isasymAnd}\mbox{n}\ \mbox{i}\ \mbox{nat}.\isanewline
 \ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}\mbox{m}.\ \mbox{m}\ <\ \mbox{n}\ {\isasymlongrightarrow}\ ({\isasymforall}\mbox{i}.\ \mbox{m}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i});\ \mbox{i}\ =\ Suc\ \mbox{nat}{\isasymrbrakk}\isanewline
 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ \mbox{n}\ =\ f\ \mbox{i}\ {\isasymlongrightarrow}\ \mbox{i}\ {\isasymle}\ f\ \mbox{i}
-\end{isabellepar}%%
+\end{isabelle}%
 \end{isamarkuptxt}%
 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
 \begin{isamarkuptext}%