src/HOL/Auth/Yahalom.thy

--- a/src/HOL/Auth/Yahalom.thy	Fri Nov 01 18:28:19 1996 +0100
+++ b/src/HOL/Auth/Yahalom.thy	Fri Nov 01 18:34:34 1996 +0100
@@ -59,7 +59,8 @@
           ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
 
          (*This message models possible leaks of session keys.  The Nonces
-           identify the protocol run.*)
+           identify the protocol run.  Quoting Server here ensures they are
+           correct.*)
     Oops "[| evs: yahalom lost;  A ~= Spy;
              Says Server A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} 
                                    (shrK A),