src/HOL/Auth/Yahalom2.thy
changeset 5359 bd539b72d484
parent 5066 30271d90644f
child 5434 9b4bed3f394c
     1.1 --- a/src/HOL/Auth/Yahalom2.thy	Fri Aug 21 15:56:12 1998 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Fri Aug 21 16:14:34 1998 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4           (*This message models possible leaks of session keys.  The nonces
     1.5             identify the protocol run.  Quoting Server here ensures they are
     1.6             correct. *)
     1.7 -    Oops "[| evso: yahalom;  A ~= Spy;
     1.8 +    Oops "[| evso: yahalom;  
     1.9               Says Server A {|Nonce NB, 
    1.10                               Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    1.11                               X|}  : set evso |]