src/HOL/Auth/OtwayRees_AN.thy

--- a/src/HOL/Auth/OtwayRees_AN.thy	Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy	Fri Aug 21 16:14:34 1998 +0200
@@ -63,7 +63,7 @@
 
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.  B is not assumed to know shrK A.*)
-    Oops "[| evso: otway;  B ~= Spy;
+    Oops "[| evso: otway;  
              Says Server B 
                       {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, 
                         Crypt (shrK B) {|Nonce NB, Agent A, Agent B, Key K|}|}