src/HOL/Auth/OtwayRees_Bad.thy
changeset 4537 4e835bd9fada
parent 4522 0218c486cf07
child 5359 bd539b72d484
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Thu Jan 08 18:10:34 1998 +0100
@@ -72,6 +72,6 @@
     Oops "[| evso: otway;  B ~= Spy;
              Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                : set evso |]
-          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
+          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : otway"
 
 end