diff -r e28870d8b223 -r a4dd02e744e0 doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Thu Dec 13 17:57:55 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Thu Dec 13 19:05:10 2001 +0100
@@ -81,12 +81,8 @@
 Additionally, you may also have to universally quantify some other variables,
 which can yield a fairly complex conclusion.  However, \isa{rule{\isacharunderscore}format} 
 can remove any number of occurrences of \isa{{\isasymforall}} and
-\isa{{\isasymlongrightarrow}}.%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isamarkupfalse%
-%
-\begin{isamarkuptext}%
+\isa{{\isasymlongrightarrow}}.
+
 \index{induction!on a term}%
 A second reason why your proposition may not be amenable to induction is that
 you want to induct on a complex term, rather than a variable. In
@@ -126,8 +122,9 @@
 Unfortunately, this induction schema cannot be expressed as a
 single theorem because it depends on the number of free variables in $t$ ---
 the notation $\overline{y}$ is merely an informal device.%
-\end{isamarkuptext}%
+\end{isamarkuptxt}%
 \isamarkuptrue%
+\isamarkupfalse%
 %
 \isamarkupsubsection{Beyond Structural and Recursion Induction%
 }