# HG changeset patch
# User paulson
# Date 845631550 -7200
# Node ID 782772e744dc15934bc16381c3d14188f07db20f
# Parent  f5c9a91e4b5002e8f101c4aba26381ae670a6f1e
Important correction to comment

diff -r f5c9a91e4b50 -r 782772e744dc src/HOL/Auth/OtwayRees.thy
--- a/src/HOL/Auth/OtwayRees.thy	Fri Oct 18 11:38:17 1996 +0200
+++ b/src/HOL/Auth/OtwayRees.thy	Fri Oct 18 11:39:10 1996 +0200
@@ -36,7 +36,7 @@
 
          (*Bob's response to Alice's message.  Bob doesn't know who 
 	   the sender is, hence the A' in the sender field.
-           We modify the published protocol by NOT encrypting NB.*)
+           Note that NB is encrypted.*)
     OR2  "[| evs: otway lost;  B ~= Server;
              Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
           ==> Says B Server