diff -r 5cd16e4df9c2 -r 6584901d694c doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Jun 23 15:26:47 2008 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Jun 23 15:26:48 2008 +0200
@@ -319,12 +319,7 @@
 \begin{quote}
 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
 \end{quote}
-where $y@1, \dots, y@n$ are variables in the first subgoal.
-The conclusion of $r$ can even be an (iterated) conjunction of formulae of
-the above form in which case the application is
-\begin{quote}
-\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{and} \dots\ \isa{and} $z@1 \dots z@m$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
-\end{quote}
+where $y@1, \dots, y@n$ are variables in the conclusion of the first subgoal.
 
 A further useful induction rule is \isa{length{\isacharunderscore}induct},
 induction on the length of a list\indexbold{*length_induct}