diff -r aea72a834c85 -r ef43a3d6e962 doc-src/TutorialI/Inductive/advanced-examples.tex
--- a/doc-src/TutorialI/Inductive/advanced-examples.tex	Thu Nov 29 21:12:37 2001 +0100
+++ b/doc-src/TutorialI/Inductive/advanced-examples.tex	Fri Nov 30 12:18:14 2001 +0100
@@ -144,8 +144,10 @@
 \isakeyword{monos}\ lists_mono
 \end{isabelle}
 
-We must cite the theorem \isa{lists_mono} in order to justify 
-using the function \isa{lists}. 
+We cite the theorem \isa{lists_mono} to justify 
+using the function \isa{lists}.%
+\footnote{This particular theorem is installed by default already, but we
+include the \isakeyword{monos} declaration in order to illustrate its syntax.}
 \begin{isabelle}
 A\ \isasymsubseteq\ B\ \isasymLongrightarrow \ lists\ A\ \isasymsubseteq
 \ lists\ B\rulenamedx{lists_mono}