1.1 --- a/src/HOL/Auth/Yahalom2.thy	Thu Jun 26 11:58:05 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Thu Jun 26 13:20:50 1997 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4           (*Bob's response to Alice's message.  Bob doesn't know who 
     1.5  	   the sender is, hence the A' in the sender field.*)
     1.6      YM2  "[| evs: yahalom lost;  B ~= Server;  Nonce NB ~: used evs;
     1.7 -             Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
     1.8 +             Says A' B {|Agent A, Nonce NA|} : set evs |]
     1.9            ==> Says B Server 
    1.10                    {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
    1.11                  # evs : yahalom lost"
    1.12 @@ -46,7 +46,7 @@
    1.13      YM3  "[| evs: yahalom lost;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
    1.14               Says B' Server {|Agent B, Nonce NB,
    1.15  			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
    1.16 -               : set_of_list evs |]
    1.17 +               : set evs |]
    1.18            ==> Says Server A
    1.19                 {|Nonce NB, 
    1.20                   Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
    1.21 @@ -58,8 +58,8 @@
    1.22      YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
    1.23               Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    1.24                          X|}
    1.25 -               : set_of_list evs;
    1.26 -             Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
    1.27 +               : set evs;
    1.28 +             Says A B {|Agent A, Nonce NA|} : set evs |]
    1.29            ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
    1.30  
    1.31           (*This message models possible leaks of session keys.  The nonces
    1.32 @@ -68,7 +68,7 @@
    1.33      Oops "[| evs: yahalom lost;  A ~= Spy;
    1.34               Says Server A {|Nonce NB, 
    1.35                               Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    1.36 -                             X|}  : set_of_list evs |]
    1.37 +                             X|}  : set evs |]
    1.38            ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
    1.39  
    1.40  end