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