src/HOL/Auth/WooLam.thy
changeset 3519 ab0a9fbed4c0
parent 3481 256f38c01b98
child 3659 eddedfe2f3f8
     1.1 --- a/src/HOL/Auth/WooLam.thy	Mon Jul 14 12:44:09 1997 +0200
     1.2 +++ b/src/HOL/Auth/WooLam.thy	Mon Jul 14 12:47:21 1997 +0200
     1.3 @@ -16,8 +16,7 @@
     1.4  
     1.5  WooLam = Shared + 
     1.6  
     1.7 -consts  lost    :: agent set        (*No need for it to be a variable*)
     1.8 -	woolam  :: event list set
     1.9 +consts  woolam  :: event list set
    1.10  inductive woolam
    1.11    intrs 
    1.12           (*Initial trace is empty*)
    1.13 @@ -27,7 +26,7 @@
    1.14             invent new nonces here, but he can also use NS1.  Common to
    1.15             all similar protocols.*)
    1.16      Fake "[| evs: woolam;  B ~= Spy;  
    1.17 -             X: synth (analz (sees lost Spy evs)) |]
    1.18 +             X: synth (analz (sees Spy evs)) |]
    1.19            ==> Says Spy B X  # evs : woolam"
    1.20  
    1.21           (*Alice initiates a protocol run*)