changeset 3683 | aafe719dff14 |
parent 3659 | eddedfe2f3f8 |
child 4552 | bb8ff763c93d |
--- a/src/HOL/Auth/Recur.thy Wed Sep 17 16:40:52 1997 +0200 +++ b/src/HOL/Auth/Recur.thy Thu Sep 18 13:24:04 1997 +0200 @@ -57,7 +57,7 @@ (*The spy MAY say anything he CAN say. Common to all similar protocols.*) Fake "[| evs: recur; B ~= Spy; - X: synth (analz (sees Spy evs)) |] + X: synth (analz (spies evs)) |] ==> Says Spy B X # evs : recur" (*Alice initiates a protocol run.