src/HOL/Auth/OtwayRees_AN.thy
changeset 3683 aafe719dff14
parent 3659 eddedfe2f3f8
child 4537 4e835bd9fada
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Wed Sep 17 16:40:52 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Thu Sep 18 13:24:04 1997 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4             invent new nonces here, but he can also use NS1.  Common to
     1.5             all similar protocols.*)
     1.6      Fake "[| evs: otway;  B ~= Spy;  
     1.7 -             X: synth (analz (sees Spy evs)) |]
     1.8 +             X: synth (analz (spies evs)) |]
     1.9            ==> Says Spy B X  # evs : otway"
    1.10  
    1.11           (*Alice initiates a protocol run*)