--- a/src/HOL/Auth/OtwayRees_AN.thy Tue Mar 09 12:20:22 1999 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy Wed Mar 10 10:42:11 1999 +0100
@@ -40,8 +40,7 @@
OR1 "[| evs1: otway |]
==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 : otway"
- (*Bob's response to Alice's message. Bob doesn't know who
- the sender is, hence the A' in the sender field.*)
+ (*Bob's response to Alice's message.*)
OR2 "[| evs2: otway;
Gets B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}