src/HOL/Auth/NS_Shared.thy
changeset 4537 4e835bd9fada
parent 3683 aafe719dff14
child 5359 bd539b72d484
--- a/src/HOL/Auth/NS_Shared.thy	Thu Jan 08 18:09:47 1998 +0100
+++ b/src/HOL/Auth/NS_Shared.thy	Thu Jan 08 18:10:34 1998 +0100
@@ -75,6 +75,6 @@
              Says B A (Crypt K (Nonce NB)) : set evso;
              Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
                : set evso |]
-          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
+          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
 
 end