src/HOL/Auth/OtwayRees.thy

--- a/src/HOL/Auth/OtwayRees.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Auth/OtwayRees.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -61,7 +61,7 @@
                  # evs3 : otway"
 
          (*Bob receives the Server's (?) message and compares the Nonces with
-	   those in the message he previously sent the Server.
+           those in the message he previously sent the 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',