src/HOL/Auth/TLS.thy

--- a/src/HOL/Auth/TLS.thy	Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/TLS.thy	Fri Aug 21 16:14:34 1998 +0200
@@ -88,7 +88,7 @@
 
     SpyKeys (*The spy may apply PRF & sessionK to available nonces*)
          "[| evsSK: tls;
-	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
+	     {Nonce NA, Nonce NB, Nonce M} <= analz (spies evsSK) |]
           ==> Notes Spy {| Nonce (PRF(M,NA,NB)),
 			   Key (sessionK((NA,NB,M),b)) |} # evsSK : tls"