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