# HG changeset patch
# User paulson
# Date 848585949 -3600
# Node ID f869dc8858413cf307b7a1dae969517353944606
# Parent  a96a7b6c04377fb6b63c545ba223896672e0a0ce
Minor reformatting

diff -r a96a7b6c0437 -r f869dc885841 src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Thu Nov 21 15:12:39 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Thu Nov 21 15:19:09 1996 +0100
@@ -596,13 +596,13 @@
 
 
 goal thy 
- "!!evs. [| B ~: lost;  evs : otway lost |]                    \
-\        ==> Says Server B                                                 \
-\              {|NA, Crypt {|NA, Key K|} (shrK A),                         \
-\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs -->      \
-\            (EX X. Says B Server {|NA, Agent A, Agent B, X,              \
-\                            Crypt {|NA, NB, Agent A, Agent B|}     \
-\                                  (shrK B)|}                       \
+ "!!evs. [| B ~: lost;  evs : otway lost |]                           \
+\        ==> Says Server B                                            \
+\              {|NA, Crypt {|NA, Key K|} (shrK A),                    \
+\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
+\            (EX X. Says B Server {|NA, Agent A, Agent B, X,          \
+\                            Crypt {|NA, NB, Agent A, Agent B|}       \
+\                                  (shrK B)|}                         \
 \            : set_of_list evs)";
 by (etac otway.induct 1);
 by (Auto_tac());
@@ -622,8 +622,8 @@
 \            : set_of_list evs;                                    \
 \           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |] \
 \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
-\                            Crypt {|NA, NB, Agent A, Agent B|}    \
-\                                  (shrK B)|}                      \
+\                                     Crypt {|NA, NB, Agent A, Agent B|}    \
+\                                           (shrK B)|}                      \
 \            : set_of_list evs";
 by (fast_tac (!claset addSDs  [A_trust_OR4]
 	              addSEs [OR3_imp_OR2]) 1);