--- a/src/HOL/Auth/OtwayRees.thy Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Thu Mar 29 10:44:37 2001 +0200
@@ -60,8 +60,8 @@
(*Bob receives the Server's (?) message and compares the Nonces with
those in the message he previously sent the Server.
- Need B ~= Server because we allow messages to self.*)
- OR4 "[| evs4 \\<in> otway; B ~= Server;
+ Need B \\<noteq> Server because we allow messages to self.*)
+ OR4 "[| evs4 \\<in> otway; B \\<noteq> Server;
Says B Server {|Nonce NA, Agent A, Agent B, X',
Crypt (shrK B)
{|Nonce NA, Nonce NB, Agent A, Agent B|}|}