src/HOL/Auth/Yahalom.thy

--- a/src/HOL/Auth/Yahalom.thy	Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Fri Aug 21 16:14:34 1998 +0200
@@ -60,7 +60,7 @@
          (*This message models possible leaks of session keys.  The Nonces
            identify the protocol run.  Quoting Server here ensures they are
            correct.*)
-    Oops "[| evso: yahalom;  A ~= Spy;
+    Oops "[| evso: yahalom;  
              Says Server A {|Crypt (shrK A)
                                    {|Agent B, Key K, Nonce NA, Nonce NB|},
                              X|}  : set evso |]