changeset 4537 | 4e835bd9fada |
parent 3683 | aafe719dff14 |
child 5359 | bd539b72d484 |
--- a/src/HOL/Auth/OtwayRees_AN.thy Thu Jan 08 18:09:47 1998 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.thy Thu Jan 08 18:10:34 1998 +0100 @@ -68,6 +68,6 @@ {|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}, Crypt (shrK B) {|Nonce NB, Agent A, Agent B, 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