--- 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\