diff -r b736de4cb913 -r 51bcafc7bfca doc-src/TutorialI/Inductive/advanced-examples.tex
--- a/doc-src/TutorialI/Inductive/advanced-examples.tex	Thu Apr 19 15:42:53 2001 +0200
+++ b/doc-src/TutorialI/Inductive/advanced-examples.tex	Fri Apr 20 11:11:40 2001 +0200
@@ -266,9 +266,13 @@
 sets
 \isa{F} and~\isa{G} then it is also a ground term over their intersection,
 \isa{F\isasyminter G}.
-
+\begin{isabelle}
+\isacommand{lemma}\ gterms_IntI:\isanewline
+\ \ \ \ \ "t\ \isasymin \ gterms\ F\ \isasymLongrightarrow \ t\ \isasymin \ gterms\ G\ \isasymlongrightarrow \ t\ \isasymin \ gterms\ (F\isasyminter
+G)"
+\end{isabelle}
 Attempting this proof, we get the assumption 
-\isa{Apply\ f\ args\ \isasymin\ gterms\ F}, which cannot be broken down. 
+\isa{Apply\ f\ args\ \isasymin\ gterms\ G}, which cannot be broken down. 
 It looks like a job for rule inversion:
 \begin{isabelle}
 \isacommand{inductive\_cases}\ gterm_Apply_elim\ [elim!]:\ "Apply\ f\ args\
@@ -326,18 +330,6 @@
 \ \ \ \ \ "gterms\ (F\isasyminter G)\ =\ gterms\ F\ \isasyminter \ gterms\ G"\isanewline
 \isacommand{by}\ (blast\ intro!:\ mono_Int\ monoI\ gterms_mono)
 \end{isabelle}
-The \isa{intro!}\ attribute of \isa{gterms_IntI} makes it available for
-this proof.
-
-
-\begin{exercise}
-Prove this theorem, one direction of which was proved in
-{\S}\ref{sec:rule-inversion} above.
-\begin{isabelle}
-\isacommand{lemma}\ gterms_Int_eq\ [simp]:\ "gterms\ (F\isasyminter G)\ =\
-gterms\ F\ \isasyminter \ gterms\ G"\isanewline
-\end{isabelle}
-\end{exercise}
 
 
 \begin{exercise}