diff -r 368414099877 -r a5604ff1ef4e doc-src/TutorialI/Protocol/protocol.tex
--- a/doc-src/TutorialI/Protocol/protocol.tex	Tue Dec 18 16:14:56 2001 +0100
+++ b/doc-src/TutorialI/Protocol/protocol.tex	Tue Dec 18 16:44:00 2001 +0100
@@ -488,7 +488,9 @@
 it is known to the spy.  Intuitively, it holds because honest agents
 always choose fresh values as nonces; only the spy might reuse a value,
 and he doesn't know this particular value.  The proof script is short:
-induction, simplification, \isa{blast}.
+induction, simplification, \isa{blast}.  The first line uses the rule
+\isa{rev_mp} to prepare the induction by moving two assumptions into the 
+induction formula.
 \begin{isabelle}
 \isacommand{lemma}\ no_nonce_NS1_NS2:\isanewline
 \ \ \ \ "\isasymlbrakk Crypt\ (pubK\ C)\ \isasymlbrace NA',\ Nonce\