src/HOL/Auth/Yahalom2.thy
changeset 4537 4e835bd9fada
parent 3683 aafe719dff14
child 5066 30271d90644f
     1.1 --- a/src/HOL/Auth/Yahalom2.thy	Thu Jan 08 18:09:47 1998 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Thu Jan 08 18:10:34 1998 +0100
     1.3 @@ -68,6 +68,6 @@
     1.4               Says Server A {|Nonce NB, 
     1.5                               Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
     1.6                               X|}  : set evso |]
     1.7 -          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
     1.8 +          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
     1.9  
    1.10  end