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