# HG changeset patch
# User paulson
# Date 867401233 -7200
# Node ID 30791e5a69c4c15033cfd9557d4c6f78e2cadc0d
# Parent  e85c24717cada76ecc5e8715e445b74f026c4c0b
Corrected indentations and margins after the renaming of "set_of_list"

diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/NS_Public.ML
--- a/src/HOL/Auth/NS_Public.ML	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/NS_Public.ML	Fri Jun 27 10:47:13 1997 +0200
@@ -134,7 +134,7 @@
 
 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
 goal thy 
- "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
+ "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;         \
 \           A ~: lost;  B ~: lost;  evs : ns_public |]                        \
 \        ==>  Nonce NA ~: analz (sees lost Spy evs)";
 by (etac rev_mp 1);
@@ -157,11 +157,11 @@
 (*Authentication for A: if she receives message 2 and has used NA
   to start a run, then B has sent message 2.*)
 goal thy 
- "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;\
-\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\             : set evs;\
-\           A ~: lost;  B ~: lost;  evs : ns_public |]  \
-\        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
+ "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs; \
+\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})  \
+\             : set evs;                                               \
+\           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
+\        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})  \
 \              : set evs";
 by (etac rev_mp 1);
 (*prepare induction over Crypt (pubK A) {|NA,NB,B|} : parts H*)
@@ -237,7 +237,7 @@
 (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
 goal thy 
  "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\             : set evs;                                      \
+\             : set evs;                                              \
 \           A ~: lost;  B ~: lost;  evs : ns_public |]                \
 \ ==> Nonce NB ~: analz (sees lost Spy evs)";
 by (etac rev_mp 1);
@@ -262,8 +262,8 @@
   in message 2, then A has sent message 3.*)
 goal thy 
  "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\             : set evs;                                       \
-\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;    \
+\             : set evs;                                               \
+\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
 \           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
 \        ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
 by (etac rev_mp 1);
@@ -294,8 +294,8 @@
   NA, then A initiated the run using NA.  SAME proof as B_trusts_NS3!*)
 goal thy 
  "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
-\             : set evs;                                       \
-\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;    \
+\             : set evs;                                               \
+\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
 \           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
 \    ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs";
 by (etac rev_mp 1);
diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/NS_Public.thy
--- a/src/HOL/Auth/NS_Public.thy	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/NS_Public.thy	Fri Jun 27 10:47:13 1997 +0200
@@ -31,8 +31,7 @@
 
          (*Bob responds to Alice's message with a further nonce*)
     NS2  "[| evs: ns_public;  A ~= B;  Nonce NB ~: used evs;
-             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
-               : set evs |]
+             Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs |]
           ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
                 # evs  :  ns_public"
 
diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/NS_Public_Bad.ML
--- a/src/HOL/Auth/NS_Public_Bad.ML	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Fri Jun 27 10:47:13 1997 +0200
@@ -139,7 +139,7 @@
 
 (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
 goal thy 
- "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \
+ "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;         \
 \           A ~: lost;  B ~: lost;  evs : ns_public |]                        \
 \        ==>  Nonce NA ~: analz (sees lost Spy evs)";
 by (etac rev_mp 1);
@@ -162,9 +162,9 @@
 (*Authentication for A: if she receives message 2 and has used NA
   to start a run, then B has sent message 2.*)
 goal thy 
- "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;\
-\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs;\
-\           A ~: lost;  B ~: lost;  evs : ns_public |]  \
+ "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs;  \
+\           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs;  \
+\           A ~: lost;  B ~: lost;  evs : ns_public |]                  \
 \        ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs";
 by (etac rev_mp 1);
 (*prepare induction over Crypt (pubK A) {|NA,NB|} : parts H*)
@@ -240,9 +240,9 @@
 
 (*NB remains secret PROVIDED Alice never responds with round 3*)
 goal thy 
- "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs;\
-\          (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs);  \
-\          A ~: lost;  B ~: lost;  evs : ns_public |]   \
+ "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs;  \
+\          (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs);    \
+\          A ~: lost;  B ~: lost;  evs : ns_public |]                   \
 \       ==> Nonce NB ~: analz (sees lost Spy evs)";
 by (etac rev_mp 1);
 by (etac rev_mp 1);
@@ -270,8 +270,8 @@
   in message 2, then A has sent message 3--to somebody....*)
 goal thy 
  "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB|})          \
-\             : set evs;                                       \
-\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;    \
+\             : set evs;                                               \
+\           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
 \           A ~: lost;  B ~: lost;  evs : ns_public |]                 \
 \        ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set evs";
 by (etac rev_mp 1);
@@ -294,7 +294,7 @@
 
 (*Can we strengthen the secrecy theorem?  NO*)
 goal thy 
- "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]   \
+ "!!evs. [| A ~: lost;  B ~: lost;  evs : ns_public |]           \
 \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \
 \     --> Nonce NB ~: analz (sees lost Spy evs)";
 by (analz_induct_tac 1);
diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Fri Jun 27 10:47:13 1997 +0200
@@ -21,7 +21,7 @@
 
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
- "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
+ "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
 \        ==> EX N K. EX evs: ns_shared lost.          \
 \               Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -38,7 +38,7 @@
 by (rtac subsetI 1);
 by (etac ns_shared.induct 1);
 by (REPEAT_FIRST
-    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
                               :: ns_shared.intrs))));
 qed "ns_shared_mono";
 
@@ -128,7 +128,7 @@
 (*Describes the form of K, X and K' when the Server sends this message.*)
 goal thy 
  "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) \
-\             : set evs;                              \
+\             : set evs;                                      \
 \           evs : ns_shared lost |]                           \
 \        ==> K ~: range shrK &                                \
 \            X = (Crypt (shrK B) {|Key K, Agent A|}) &        \
@@ -161,7 +161,7 @@
   Use Says_Server_message_form if applicable.*)
 goal thy 
  "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
-\            : set evs;  evs : ns_shared lost |]                   \
+\            : set evs;          evs : ns_shared lost |]                   \
 \        ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|}))   \
 \            | X : analz (sees lost Spy evs)";
 by (case_tac "A : lost" 1);
@@ -195,9 +195,9 @@
   to encrypt messages containing other keys, in the actual protocol.
   We require that agents should behave like this subsequently also.*)
 goal thy 
- "!!evs. [| evs : ns_shared lost;  Kab ~: range shrK |] ==> \
-\        (Crypt KAB X) : parts (sees lost Spy evs) & \
-\        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
+ "!!evs. [| evs : ns_shared lost;  Kab ~: range shrK |] ==>  \
+\           (Crypt KAB X) : parts (sees lost Spy evs) &      \
+\           Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
 by parts_induct_tac;
 (*Deals with Faked messages*)
 by (blast_tac (!claset addSEs partsEs
@@ -211,9 +211,9 @@
 
 (*The equality makes the induction hypothesis easier to apply*)
 goal thy  
- "!!evs. evs : ns_shared lost ==> \
-\  ALL K KK. KK <= Compl (range shrK) -->                      \
-\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+ "!!evs. evs : ns_shared lost ==>                                \
+\  ALL K KK. KK <= Compl (range shrK) -->                        \
+\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
 \            (K : KK | Key K : analz (sees lost Spy evs))";
 by (etac ns_shared.induct 1);
 by analz_sees_tac;
@@ -242,7 +242,7 @@
  "!!evs. evs : ns_shared lost ==>                                        \
 \      EX A' NA' B' X'. ALL A NA B X.                                    \
 \       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})         \
-\       : set evs --> A=A' & NA=NA' & B=B' & X=X'";
+\       : set evs -->         A=A' & NA=NA' & B=B' & X=X'";
 by (etac ns_shared.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
 by (Step_tac 1);
@@ -260,10 +260,10 @@
 goal thy 
  "!!evs. [| Says Server A                                    \
 \             (Crypt (shrK A) {|NA, Agent B, Key K, X|})     \
-\                  : set evs;                        \ 
+\                  : set evs;                                \ 
 \           Says Server A'                                   \
 \             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) \
-\                  : set evs;                        \
+\                  : set evs;                                \
 \           evs : ns_shared lost |] ==> A=A' & NA=NA' & B=B' & X = X'";
 by (prove_unique_tac lemma 1);
 qed "unique_session_keys";
@@ -276,8 +276,8 @@
 \        ==> Says Server A                                             \
 \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
 \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
-\             : set evs -->                                    \
-\        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) --> \
+\             : set evs -->                                            \
+\        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs) -->         \
 \        Key K ~: analz (sees lost Spy evs)";
 by (etac ns_shared.induct 1);
 by analz_sees_tac;
@@ -308,8 +308,8 @@
 (*Final version: Server's message in the most abstract form*)
 goal thy 
  "!!evs. [| Says Server A                                               \
-\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;    \
-\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);  \
+\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
+\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
 \           A ~: lost;  B ~: lost;  evs : ns_shared lost                \
 \        |] ==> Key K ~: analz (sees lost Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -320,8 +320,8 @@
 goal thy 
  "!!evs. [| C ~: {A,B,Server};                                          \
 \           Says Server A                                               \
-\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;    \
-\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);  \
+\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
+\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
 \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]             \
 \        ==> Key K ~: analz (sees lost C evs)";
 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -354,11 +354,11 @@
 
 
 goal thy
- "!!evs. [| B ~: lost;  evs : ns_shared lost |]            \
-\        ==> Key K ~: analz (sees lost Spy evs) -->             \
+ "!!evs. [| B ~: lost;  evs : ns_shared lost |]                        \
+\        ==> Key K ~: analz (sees lost Spy evs) -->                    \
 \            Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
-\            : set evs --> \
-\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->            \
+\            : set evs -->                                             \
+\            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->        \
 \            Says B A (Crypt K (Nonce NB)) : set evs";
 by (etac ns_shared.induct 1);
 by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
@@ -390,8 +390,8 @@
 goal thy
  "!!evs. [| Crypt K (Nonce NB) : parts (sees lost Spy evs);           \
 \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
-\           : set evs;                                        \
-\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;  \
+\           : set evs;                                                \
+\           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs;          \
 \           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
 \        ==> Says B A (Crypt K (Nonce NB)) : set evs";
 by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Fri Jun 27 10:47:13 1997 +0200
@@ -150,7 +150,7 @@
   for Oops case.*)
 goal thy 
  "!!evs. [| Says Server B                                                 \
-\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
+\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;           \
 \           evs : otway lost |]                                           \
 \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
 by (etac rev_mp 1);
@@ -183,9 +183,9 @@
 
 (*The equality makes the induction hypothesis easier to apply*)
 goal thy  
- "!!evs. evs : otway lost ==>                                         \
-\  ALL K KK. KK <= Compl (range shrK) -->                      \
-\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+ "!!evs. evs : otway lost ==>                                    \
+\  ALL K KK. KK <= Compl (range shrK) -->                        \
+\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
 \            (K : KK | Key K : analz (sees lost Spy evs))";
 by (etac otway.induct 1);
 by analz_sees_tac;
@@ -200,8 +200,8 @@
 
 
 goal thy
- "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>             \
-\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+ "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>          \
+\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =  \
 \        (K = KAB | Key K : analz (sees lost Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
@@ -210,9 +210,9 @@
 (*** The Key K uniquely identifies the Server's  message. **)
 
 goal thy 
- "!!evs. evs : otway lost ==>                                                 \
-\   EX B' NA' NB' X'. ALL B NA NB X.                                          \
-\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
+ "!!evs. evs : otway lost ==>                                             \
+\   EX B' NA' NB' X'. ALL B NA NB X.                                      \
+\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs -->     \
 \     B=B' & NA=NA' & NB=NB' & X=X'";
 by (etac otway.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -229,9 +229,9 @@
 
 goal thy 
  "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
-\            : set evs;                                    \ 
+\            : set evs;                                            \ 
 \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
-\            : set evs;                                    \
+\            : set evs;                                            \
 \           evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
 by (prove_unique_tac lemma 1);
 qed "unique_session_keys";
@@ -257,7 +257,7 @@
 
 goal thy 
  "!!evs. [| evs : otway lost; A ~: lost |]               \
-\ ==> EX B'. ALL B.    \
+\ ==> EX B'. ALL B.                                      \
 \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
 \        --> B = B'";
 by parts_induct_tac;
@@ -300,7 +300,7 @@
 \    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs)      \
 \        --> Says A B {|NA, Agent A, Agent B,                          \
 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
-\             : set evs -->                                    \
+\             : set evs -->                                            \
 \            (EX NB. Says Server B                                     \
 \                 {|NA,                                                \
 \                   Crypt (shrK A) {|NA, Key K|},                      \
@@ -335,10 +335,10 @@
   Spy_not_see_encrypted_key*)
 goal thy 
  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
-\            : set evs;                                    \
+\            : set evs;                                            \
 \           Says A B {|NA, Agent A, Agent B,                       \
 \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
-\            : set evs;                                    \
+\            : set evs;                                            \
 \           A ~: lost;  A ~= Spy;  evs : otway lost |]             \
 \        ==> EX NB. Says Server B                                  \
 \                     {|NA,                                        \
@@ -358,8 +358,8 @@
  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
 \        ==> Says Server B                                                 \
 \              {|NA, Crypt (shrK A) {|NA, Key K|},                         \
-\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->      \
-\            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
+\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->              \
+\            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac otway.induct 1);
 by analz_sees_tac;
@@ -382,8 +382,8 @@
 goal thy 
  "!!evs. [| Says Server B                                                \
 \            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
-\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;     \
-\           Says B Spy {|NA, NB, Key K|} ~: set evs;             \
+\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;             \
+\           Says B Spy {|NA, NB, Key K|} ~: set evs;                     \
 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
 \        ==> Key K ~: analz (sees lost Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -395,8 +395,8 @@
  "!!evs. [| C ~: {A,B,Server};                                           \
 \           Says Server B                                                \
 \            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
-\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;     \
-\           Says B Spy {|NA, NB, Key K|} ~: set evs;             \
+\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;             \
+\           Says B Spy {|NA, NB, Key K|} ~: set evs;                     \
 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
 \        ==> Key K ~: analz (sees lost C evs)";
 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -458,7 +458,7 @@
 \        --> (ALL X'. Says B Server                                      \
 \                       {|NA, Agent A, Agent B, X',                      \
 \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
-\             : set evs                                          \
+\             : set evs                                                  \
 \             --> Says Server B                                          \
 \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
 \                        Crypt (shrK B) {|NB, Key K|}|}                  \
@@ -486,10 +486,10 @@
 goal thy 
  "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
 \           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}      \
-\            : set evs;                                    \
+\            : set evs;                                            \
 \           Says B Server {|NA, Agent A, Agent B, X',              \
 \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
-\            : set evs |]                                  \
+\            : set evs |]                                          \
 \        ==> Says Server B                                         \
 \                 {|NA,                                            \
 \                   Crypt (shrK A) {|NA, Key K|},                  \
@@ -507,7 +507,7 @@
  "!!evs. [| B ~: lost;  evs : otway lost |]                           \
 \        ==> Says Server B                                            \
 \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
-\                Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
+\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
 \            (EX X. Says B Server {|NA, Agent A, Agent B, X,          \
 \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
 \            : set evs)";
@@ -523,13 +523,11 @@
   We could probably prove that X has the expected form, but that is not
   strictly necessary for authentication.*)
 goal thy 
- "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
-\            : set evs;                                    \
-\           Says A B {|NA, Agent A, Agent B,                       \
-\                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
-\            : set evs;                                    \
-\           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |] \
-\        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
+ "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;       \
+\           Says A B {|NA, Agent A, Agent B,                                \
+\                      Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
+\           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |]          \
+\        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,              \
 \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
 \            : set evs";
 by (blast_tac (!claset addSDs  [A_trusts_OR4]
diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Jun 27 10:47:13 1997 +0200
@@ -139,7 +139,7 @@
  "!!evs. [| Says Server B                                           \
 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
-\             : set evs;                                    \
+\             : set evs;                                            \
 \           evs : otway lost |]                                     \
 \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
 by (etac rev_mp 1);
@@ -171,9 +171,9 @@
 
 (*The equality makes the induction hypothesis easier to apply*)
 goal thy  
- "!!evs. evs : otway lost ==>                                         \
-\  ALL K KK. KK <= Compl (range shrK) -->                      \
-\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+ "!!evs. evs : otway lost ==>                                    \
+\  ALL K KK. KK <= Compl (range shrK) -->                        \
+\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
 \            (K : KK | Key K : analz (sees lost Spy evs))";
 by (etac otway.induct 1);
 by analz_sees_tac;
@@ -188,8 +188,8 @@
 
 
 goal thy
- "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>             \
-\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+ "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>          \
+\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =  \
 \        (K = KAB | Key K : analz (sees lost Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
@@ -200,8 +200,8 @@
 goal thy 
  "!!evs. evs : otway lost ==>                              \
 \      EX A' B' NA' NB'. ALL A B NA NB.                    \
-\       Says Server B \
-\         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},                     \
+\       Says Server B                                      \
+\         {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},             \
 \           Crypt (shrK B) {|NB, Agent A, Agent B, K|}|} : set evs  \
 \       --> A=A' & B=B' & NA=NA' & NB=NB'";
 by (etac otway.induct 1);
@@ -222,11 +222,11 @@
 "!!evs. [| Says Server B                                           \
 \            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},         \
 \              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}        \
-\           : set evs;                                     \
+\           : set evs;                                             \
 \          Says Server B'                                          \
 \            {|Crypt (shrK A') {|NA', Agent A', Agent B', K|},     \
 \              Crypt (shrK B') {|NB', Agent A', Agent B', K|}|}    \
-\           : set evs;                                     \
+\           : set evs;                                             \
 \          evs : otway lost |]                                     \
 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
 by (prove_unique_tac lemma 1);
@@ -257,7 +257,7 @@
   Freshness may be inferred from nonce NA.*)
 goal thy 
  "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
-\            : set evs;                                         \
+\            : set evs;                                                 \
 \           A ~: lost;  evs : otway lost |]                             \
 \        ==> EX NB. Says Server B                                       \
 \                    {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},  \
@@ -277,8 +277,8 @@
 \        ==> Says Server B                                                 \
 \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},            \
 \               Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}           \
-\            : set evs -->                                         \
-\            Says B Spy {|NA, NB, Key K|} ~: set evs -->           \
+\            : set evs -->                                                 \
+\            Says B Spy {|NA, NB, Key K|} ~: set evs -->                   \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac otway.induct 1);
 by analz_sees_tac;
@@ -302,8 +302,8 @@
  "!!evs. [| Says Server B                                           \
 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
-\             : set evs;                                    \
-\           Says B Spy {|NA, NB, Key K|} ~: set evs;        \
+\             : set evs;                                            \
+\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
 \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
 \        ==> Key K ~: analz (sees lost Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -316,8 +316,8 @@
 \           Says Server B                                           \
 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
-\             : set evs;                                    \
-\           Says B Spy {|NA, NB, Key K|} ~: set evs;        \
+\             : set evs;                                            \
+\           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
 \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
 \        ==> Key K ~: analz (sees lost C evs)";
 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -351,7 +351,7 @@
 goal thy 
  "!!evs. [| B ~: lost;  evs : otway lost;                                   \
 \           Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
-\            : set evs |]                                           \
+\            : set evs |]                                                   \
 \        ==> EX NA. Says Server B                                           \
 \                     {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},     \
 \                       Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}    \
diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/OtwayRees_AN.thy
--- a/src/HOL/Auth/OtwayRees_AN.thy	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy	Fri Jun 27 10:47:13 1997 +0200
@@ -56,8 +56,7 @@
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.*)
     OR4  "[| evs: otway lost;  A ~= B;
-             Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
-               : set evs;
+             Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs;
              Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
                : set evs |]
           ==> Says B A X # evs : otway lost"
diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Fri Jun 27 10:47:13 1997 +0200
@@ -140,7 +140,7 @@
   for Oops case.*)
 goal thy 
  "!!evs. [| Says Server B                                                 \
-\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
+\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;           \
 \           evs : otway |]                                                \
 \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
 by (etac rev_mp 1);
@@ -172,9 +172,9 @@
 
 (*The equality makes the induction hypothesis easier to apply*)
 goal thy  
- "!!evs. evs : otway ==> \
-\  ALL K KK. KK <= Compl (range shrK) -->                      \
-\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+ "!!evs. evs : otway ==>                                         \
+\  ALL K KK. KK <= Compl (range shrK) -->                        \
+\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
 \            (K : KK | Key K : analz (sees lost Spy evs))";
 by (etac otway.induct 1);
 by analz_sees_tac;
@@ -199,9 +199,9 @@
 (*** The Key K uniquely identifies the Server's  message. **)
 
 goal thy 
- "!!evs. evs : otway ==>                                                      \
-\   EX B' NA' NB' X'. ALL B NA NB X.                                          \
-\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs --> \
+ "!!evs. evs : otway ==>                                                  \
+\   EX B' NA' NB' X'. ALL B NA NB X.                                      \
+\     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs -->     \
 \     B=B' & NA=NA' & NB=NB' & X=X'";
 by (etac otway.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
@@ -217,10 +217,8 @@
 val lemma = result();
 
 goal thy 
- "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
-\            : set evs;                                    \ 
-\           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
-\            : set evs;                                    \
+ "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
+\           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
 \           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
 by (prove_unique_tac lemma 1);
 qed "unique_session_keys";
@@ -231,8 +229,8 @@
  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                    \
 \        ==> Says Server B                                            \
 \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
-\                Crypt (shrK B) {|NB, Key K|}|} : set evs --> \
-\            Says B Spy {|NA, NB, Key K|} ~: set evs -->      \
+\                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
+\            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac otway.induct 1);
 by analz_sees_tac;
@@ -253,10 +251,10 @@
 val lemma = result() RS mp RS mp RSN(2,rev_notE);
 
 goal thy 
- "!!evs. [| Says Server B                                                \
-\            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
-\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;     \
-\           Says B Spy {|NA, NB, Key K|} ~: set evs;             \
+ "!!evs. [| Says Server B                                         \
+\            {|NA, Crypt (shrK A) {|NA, Key K|},                  \
+\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;      \
+\           Says B Spy {|NA, NB, Key K|} ~: set evs;              \
 \           A ~: lost;  B ~: lost;  evs : otway |]                \
 \        ==> Key K ~: analz (sees lost Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -275,8 +273,7 @@
 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}           \
 \             : parts (sees lost Spy evs) -->                  \
 \            Says A B {|NA, Agent A, Agent B,                  \
-\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
-\             : set evs";
+\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  : set evs";
 by parts_induct_tac;
 by (Fake_parts_insert_tac 1);
 by (Blast_tac 1);
@@ -288,16 +285,15 @@
 (*Only it is FALSE.  Somebody could make a fake message to Server
           substituting some other nonce NA' for NB.*)
 goal thy 
- "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                        \
+ "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                         \
 \        ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs) --> \
-\            Says A B {|NA, Agent A, Agent B,                  \
+\            Says A B {|NA, Agent A, Agent B,                      \
 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
-\             : set evs -->                            \
+\             : set evs -->                                    \
 \            (EX B NB. Says Server B                           \
 \                 {|NA,                                        \
 \                   Crypt (shrK A) {|NA, Key K|},              \
-\                   Crypt (shrK B) {|NB, Key K|}|}             \
-\                   : set evs)";
+\                   Crypt (shrK B) {|NB, Key K|}|}  : set evs)";
 by parts_induct_tac;
 by (Fake_parts_insert_tac 1);
 (*OR1: it cannot be a new Nonce, contradiction.*)
diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/Recur.ML	Fri Jun 27 10:47:13 1997 +0200
@@ -21,11 +21,10 @@
 
 (*Simplest case: Alice goes directly to the server*)
 goal thy
- "!!A. A ~= Server   \
+ "!!A. A ~= Server                          \
 \ ==> EX K NA. EX evs: recur lost.          \
 \     Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
-\                     Agent Server|}      \
-\         : set evs";
+\                     Agent Server|}  : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (recur.Nil RS recur.RA1 RS 
           (respond.One RSN (4,recur.RA3))) 2);
@@ -38,8 +37,7 @@
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
 \ ==> EX K. EX NA. EX evs: recur lost.            \
 \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
-\                  Agent Server|}                               \
-\         : set evs";
+\                  Agent Server|}  : set evs";
 by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
 by (REPEAT (eresolve_tac [exE, conjE] 1));
 by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -58,8 +56,7 @@
  "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |]   \
 \ ==> EX K. EX NA. EX evs: recur lost.                          \
 \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
-\                  Agent Server|}                               \
-\         : set evs";
+\                  Agent Server|}  : set evs";
 by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
 by (REPEAT (eresolve_tac [exE, conjE] 1));
 by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -82,7 +79,7 @@
 by (rtac subsetI 1);
 by (etac recur.induct 1);
 by (REPEAT_FIRST
-    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
                               :: recur.intrs))));
 qed "recur_mono";
 
@@ -528,9 +525,8 @@
 goalw thy [HPair_def]
  "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|}         \
 \             : parts (sees lost Spy evs);                        \
-\            A ~: lost;  evs : recur lost |]                        \
-\        ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|})  \
-\             : set evs";
+\            A ~: lost;  evs : recur lost |]                      \
+\     ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
 by (etac rev_mp 1);
 by parts_induct_tac;
 by (Fake_parts_insert_tac 1);
@@ -547,7 +543,7 @@
 goal thy 
  "!!evs. [| Crypt (shrK A) Y : parts (sees lost Spy evs);    \
 \           A ~: lost;  A ~= Spy;  evs : recur lost |]       \
-\        ==> EX C RC. Says Server C RC : set evs &   \
+\        ==> EX C RC. Says Server C RC : set evs  &          \
 \                     Crypt (shrK A) Y : parts {RC}";
 by (etac rev_mp 1);
 by parts_induct_tac;
diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/Recur.thy	Fri Jun 27 10:47:13 1997 +0200
@@ -90,15 +90,13 @@
            those in the message he previously sent the Server.*)
     RA4  "[| evs: recur lost;  A ~= B;  
              Says B  C {|XH, Agent B, Agent C, Nonce NB, 
-                         XA, Agent A, Agent B, Nonce NA, P|} 
-               : set evs;
+                         XA, Agent A, Agent B, Nonce NA, P|} : set evs;
              Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
                          Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
-                         RA|}
-               : set evs |]
+                         RA|} : set evs |]
           ==> Says B A RA # evs : recur lost"
 
-(**No "oops" message can readily be expressed, since each session key is
+(**No "oops" message can easily be expressed.  Each session key is
    associated--in two separate messages--with two nonces.
 ***)
 end
diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/WooLam.ML
--- a/src/HOL/Auth/WooLam.ML	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/WooLam.ML	Fri Jun 27 10:47:13 1997 +0200
@@ -21,8 +21,7 @@
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
 \        ==> EX NB. EX evs: woolam.               \
-\               Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \
-\                 : set evs";
+\              Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
           woolam.WL4 RS woolam.WL5) 2);
@@ -107,7 +106,7 @@
   Alice, then she originated that certificate.  But we DO NOT know that B
   ever saw it: the Spy may have rerouted the message to the Server.*)
 goal thy 
- "!!evs. [| A ~: lost;  evs : woolam;               \
+ "!!evs. [| A ~: lost;  evs : woolam;                      \
 \           Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
 \            : set evs |]                                  \
 \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
@@ -121,8 +120,8 @@
 
 (*Server sent WL5 only if it received the right sort of message*)
 goal thy 
- "!!evs. evs : woolam ==>                                              \
-\        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs   \
+ "!!evs. evs : woolam ==>                                                   \
+\        Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs           \
 \        --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
 \               : set evs)";
 by parts_induct_tac;
@@ -133,8 +132,8 @@
 
 (*If the encrypted message appears then it originated with the Server!*)
 goal thy 
- "!!evs. [| B ~: lost;  evs : woolam |]                   \
-\    ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs)        \
+ "!!evs. [| B ~: lost;  evs : woolam |]                                  \
+\        ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs)  \
 \        --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
 by parts_induct_tac;
 by (Fake_parts_insert_tac 1);
@@ -143,7 +142,7 @@
 (*Partial guarantee for B: if it gets a message of correct form then the Server
   sent the same message.*)
 goal thy 
- "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set evs; \
+ "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set evs;         \
 \           B ~: lost;  evs : woolam |]                                  \
 \        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
 by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
@@ -156,7 +155,7 @@
   the Server via the Spy.*)
 goal thy 
  "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \
-\           A ~: lost;  B ~: lost;  evs : woolam  |] \
+\           A ~: lost;  B ~: lost;  evs : woolam  |]                  \
 \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
 by (blast_tac (!claset addIs  [Server_trusts_WL4]
                       addSDs [B_got_WL5 RS Server_sent_WL5]) 1);
@@ -176,9 +175,9 @@
 
 (**CANNOT be proved because A doesn't know where challenges come from...
 goal thy 
- "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam |]                   \
+ "!!evs. [| A ~: lost;  B ~= Spy;  evs : woolam |]                \
 \    ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) &  \
-\        Says B A (Nonce NB) : set evs        \
+\        Says B A (Nonce NB) : set evs                            \
 \        --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
 by parts_induct_tac;
 by (Fake_parts_insert_tac 1);
diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Fri Jun 27 10:47:13 1997 +0200
@@ -23,7 +23,7 @@
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
-\        ==> EX X NB K. EX evs: yahalom lost.          \
+\        ==> EX X NB K. EX evs: yahalom lost.     \
 \               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
@@ -39,7 +39,7 @@
 by (rtac subsetI 1);
 by (etac yahalom.induct 1);
 by (REPEAT_FIRST
-    (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
+    (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
                               :: yahalom.intrs))));
 qed "yahalom_mono";
 
@@ -65,8 +65,7 @@
           YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
 
 (*Relates to both YM4 and Oops*)
-goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \
-\                  : set evs ==> \
+goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
 \                K : parts (sees lost Spy evs)";
 by (blast_tac (!claset addSEs partsEs
                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
@@ -140,7 +139,7 @@
   Oops as well as main secrecy property.*)
 goal thy 
  "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
-\             : set evs;                                           \
+\             : set evs;                                                   \
 \           evs : yahalom lost |]                                          \
 \        ==> K ~: range shrK";
 by (etac rev_mp 1);
@@ -169,8 +168,8 @@
 (** Session keys are not used to encrypt other session keys **)
 
 goal thy  
- "!!evs. evs : yahalom lost ==> \
-\  ALL K KK. KK <= Compl (range shrK) -->                      \
+ "!!evs. evs : yahalom lost ==>                                 \
+\  ALL K KK. KK <= Compl (range shrK) -->                       \
 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
 \            (K : KK | Key K : analz (sees lost Spy evs))";
 by (etac yahalom.induct 1);
@@ -186,7 +185,7 @@
 
 goal thy
  "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
-\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =       \
 \        (K = KAB | Key K : analz (sees lost Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
@@ -196,7 +195,7 @@
 
 goal thy 
  "!!evs. evs : yahalom lost ==>                                     \
-\      EX A' B' na' nb' X'. ALL A B na nb X.                             \
+\      EX A' B' na' nb' X'. ALL A B na nb X.                        \
 \          Says Server A                                            \
 \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
 \          : set evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
@@ -216,10 +215,10 @@
 goal thy 
 "!!evs. [| Says Server A                                            \
 \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
-\           : set evs;                                      \
+\           : set evs;                                              \
 \          Says Server A'                                           \
 \           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|}   \
-\           : set evs;                                      \
+\           : set evs;                                              \
 \          evs : yahalom lost |]                                    \
 \       ==> A=A' & B=B' & na=na' & nb=nb'";
 by (prove_unique_tac lemma 1);
@@ -233,8 +232,8 @@
 \        ==> Says Server A                                        \
 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
-\             : set evs -->                               \
-\            Says A Spy {|na, nb, Key K|} ~: set evs -->  \
+\             : set evs -->                                       \
+\            Says A Spy {|na, nb, Key K|} ~: set evs -->          \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac yahalom.induct 1);
 by analz_sees_tac;
@@ -259,8 +258,8 @@
  "!!evs. [| Says Server A                                         \
 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
-\             : set evs;                                  \
-\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
+\             : set evs;                                          \
+\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
 \        ==> Key K ~: analz (sees lost Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -274,8 +273,8 @@
 \           Says Server A                                         \
 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
-\             : set evs;                                  \
-\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
+\             : set evs;                                          \
+\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
 \        ==> Key K ~: analz (sees lost C evs)";
 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -394,7 +393,7 @@
 goalw thy [KeyWithNonce_def]
  "!!evs. [| Says Server A                                                \
 \                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
-\             : set evs;                                         \
+\             : set evs;                                                 \
 \           NB ~= NB';  evs : yahalom lost |]                            \
 \        ==> ~ KeyWithNonce K NB evs";
 by (blast_tac (!claset addDs [unique_session_keys]) 1);
@@ -453,7 +452,7 @@
 goal thy 
  "!!evs. [| Says Server A                                                 \
 \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}    \
-\           : set evs;                                            \
+\           : set evs;                                                    \
 \           NB ~= NB';  KAB ~: range shrK;  evs : yahalom lost |]         \
 \        ==> (Nonce NB : analz (insert (Key KAB) (sees lost Spy evs))) =  \
 \            (Nonce NB : analz (sees lost Spy evs))";
@@ -495,9 +494,9 @@
   not_lost_tac to remove the assumption B' ~: lost.*)
 goal thy 
  "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, NB|}|}    \
-\            : set evs;  B ~: lost;                               \
+\            : set evs;          B ~: lost;                               \
 \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
-\            : set evs;                                           \
+\            : set evs;                                                   \
 \          NB ~: analz (sees lost Spy evs);  evs : yahalom lost |]        \
 \        ==> NA' = NA & A' = A & B' = B";
 by (not_lost_tac "B'" 1);
@@ -527,8 +526,8 @@
 
 (*The Server sends YM3 only in response to YM2.*)
 goal thy 
- "!!evs. [| Says Server A                                           \
-\            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs; \
+ "!!evs. [| Says Server A                                                \
+\            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs;     \
 \           evs : yahalom lost |]                                        \
 \        ==> EX B'. Says B' Server                                       \
 \                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
@@ -546,8 +545,8 @@
  "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
 \ ==> Says B Server                                                    \
 \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
-\     : set evs -->                               \
-\     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->  \
+\     : set evs -->                                                    \
+\     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->     \
 \     Nonce NB ~: analz (sees lost Spy evs)";
 by (etac yahalom.induct 1);
 by analz_sees_tac;
@@ -606,10 +605,10 @@
 goal thy 
  "!!evs. [| Says B Server                                                   \
 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
-\             : set evs;                                            \
+\             : set evs;                                                    \
 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
-\                       Crypt K (Nonce NB)|} : set evs;             \
-\           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs; \
+\                       Crypt K (Nonce NB)|} : set evs;                     \
+\           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs;         \
 \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
 \         ==> Says Server A                                                 \
 \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
@@ -636,8 +635,7 @@
 \  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|}                        \
 \        : parts (sees lost Spy evs) -->                               \
 \      B ~: lost -->                                                   \
-\      Says B Server {|Agent B,                                \
-\                          Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
+\      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
 \         : set evs";
 by parts_induct_tac;
 by (Fake_parts_insert_tac 1);
@@ -645,12 +643,11 @@
 
 (*If the server sends YM3 then B sent YM2*)
 goal thy 
- "!!evs. evs : yahalom lost                                       \
+ "!!evs. evs : yahalom lost                                                 \
 \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
-\         : set evs -->                                          \
-\      B ~: lost -->                                                     \
-\      Says B Server {|Agent B,                            \
-\                               Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}   \
+\         : set evs -->                                                     \
+\      B ~: lost -->                                                        \
+\      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
 \                 : set evs";
 by (etac yahalom.induct 1);
 by (ALLGOALS Asm_simp_tac);
@@ -664,7 +661,7 @@
 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
 goal thy
  "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
-\             : set evs;                                            \
+\             : set evs;                                                    \
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
 \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
 \         : set evs";
@@ -720,11 +717,10 @@
 goal thy 
  "!!evs. [| Says B Server                                                   \
 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
-\             : set evs;                                            \
-\           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},       \
-\                       Crypt K (Nonce NB)|} : set evs;  \
-\           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|}    \
-\               ~: set evs);                             \
+\             : set evs;                                                    \
+\           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
+\                       Crypt K (Nonce NB)|} : set evs;                     \
+\           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs);    \
 \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
 \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
 by (dtac B_trusts_YM4 1);
diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.ML	Fri Jun 27 10:47:13 1997 +0200
@@ -23,7 +23,7 @@
 
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
- "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
+ "!!A B. [| A ~= B; A ~= Server; B ~= Server |]        \
 \        ==> EX X NB K. EX evs: yahalom lost.          \
 \               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -66,11 +66,10 @@
           YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
 
 (*Relates to both YM4 and Oops*)
-goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B, K, NA|}, X|} \
-\                  : set evs ==> \
+goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \
 \                K : parts (sees lost Spy evs)";
 by (blast_tac (!claset addSEs partsEs
-                      addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
+                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
 qed "YM4_Key_parts_sees_Spy";
 
 (*For proving the easier theorems about X ~: parts (sees lost Spy evs).
@@ -140,7 +139,7 @@
   Oops as well as main secrecy property.*)
 goal thy 
  "!!evs. [| Says Server A {|NB', Crypt (shrK A) {|Agent B, Key K, NA|}, X|} \
-\            : set evs;                                         \
+\            : set evs;                                                 \
 \           evs : yahalom lost |]                                       \
 \        ==> K ~: range shrK & A ~= B";
 by (etac rev_mp 1);
@@ -170,9 +169,9 @@
 (** Session keys are not used to encrypt other session keys **)
 
 goal thy  
- "!!evs. evs : yahalom lost ==> \
-\  ALL K KK. KK <= Compl (range shrK) -->                      \
-\            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+ "!!evs. evs : yahalom lost ==>                                  \
+\  ALL K KK. KK <= Compl (range shrK) -->                        \
+\            (Key K : analz (Key``KK Un (sees lost Spy evs))) =  \
 \            (K : KK | Key K : analz (sees lost Spy evs))";
 by (etac yahalom.induct 1);
 by analz_sees_tac;
@@ -187,7 +186,7 @@
 
 goal thy
  "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
-\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+\        Key K : analz (insert (Key KAB) (sees lost Spy evs)) =       \
 \        (K = KAB | Key K : analz (sees lost Spy evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
 qed "analz_insert_freshK";
@@ -216,10 +215,10 @@
 goal thy 
 "!!evs. [| Says Server A                                            \
 \           {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|}        \
-\           : set evs;                                      \
+\           : set evs;                                              \
 \          Says Server A'                                           \
 \           {|nb', Crypt (shrK A') {|Agent B', Key K, na'|}, X'|}   \
-\           : set evs;                                      \
+\           : set evs;                                              \
 \          evs : yahalom lost |]                                    \
 \       ==> A=A' & B=B' & na=na' & nb=nb'";
 by (prove_unique_tac lemma 1);
@@ -234,8 +233,8 @@
 \        ==> Says Server A                                           \
 \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},          \
 \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}         \
-\             : set evs -->                                  \
-\            Says A Spy {|na, nb, Key K|} ~: set evs -->     \
+\             : set evs -->                                          \
+\            Says A Spy {|na, nb, Key K|} ~: set evs -->             \
 \            Key K ~: analz (sees lost Spy evs)";
 by (etac yahalom.induct 1);
 by analz_sees_tac;
@@ -260,8 +259,8 @@
  "!!evs. [| Says Server A                                         \
 \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},       \
 \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}      \
-\           : set evs;                                    \
-\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
+\           : set evs;                                            \
+\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
 \        ==> Key K ~: analz (sees lost Spy evs)";
 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -275,8 +274,8 @@
 \           Says Server A                                         \
 \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},       \
 \                    Crypt (shrK B) {|nb, Key K, Agent A|}|}      \
-\           : set evs;                                    \
-\           Says A Spy {|na, nb, Key K|} ~: set evs;      \
+\           : set evs;                                            \
+\           Says A Spy {|na, nb, Key K|} ~: set evs;              \
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
 \        ==> Key K ~: analz (sees lost C evs)";
 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
@@ -333,7 +332,7 @@
   because we do not have to show that NB is secret. *)
 goal thy 
  "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|}, X|} \
-\             : set evs;                                         \
+\             : set evs;                                                 \
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                \
 \        ==> EX NA. Says Server A                                        \
 \                    {|Nonce NB,                                         \
@@ -364,9 +363,9 @@
 
 (*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
 goal thy 
- "!!evs. evs : yahalom lost                                       \
+ "!!evs. evs : yahalom lost                                              \
 \  ==> Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
-\         : set evs -->                                          \
+\         : set evs -->                                                  \
 \      B ~: lost -->                                                     \
 \      (EX nb'. Says B Server {|Agent B, nb',                            \
 \                               Crypt (shrK B) {|Agent A, Nonce NA|}|}   \
@@ -384,7 +383,7 @@
 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
 goal thy
  "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
-\             : set evs;                                            \
+\             : set evs;                                                    \
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
 \   ==> EX nb'. Says B Server                                               \
 \                    {|Agent B, nb', Crypt (shrK B) {|Agent A, Nonce NA|}|} \
@@ -440,7 +439,7 @@
   Other premises guarantee secrecy of K.*)
 goal thy 
  "!!evs. [| Says A' B {|Crypt (shrK B) {|Nonce NB, Key K, Agent A|},    \
-\                       Crypt K (Nonce NB)|} : set evs;         \
+\                       Crypt K (Nonce NB)|} : set evs;                 \
 \           (ALL NA. Says A Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \
 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
 \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
diff -r e85c24717cad -r 30791e5a69c4 src/HOL/Auth/Yahalom2.thy
--- a/src/HOL/Auth/Yahalom2.thy	Thu Jun 26 13:20:50 1997 +0200
+++ b/src/HOL/Auth/Yahalom2.thy	Fri Jun 27 10:47:13 1997 +0200
@@ -57,8 +57,7 @@
            uses the new session key to send Bob his Nonce.*)
     YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
              Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
-                        X|}
-               : set evs;
+                        X|}  : set evs;
              Says A B {|Agent A, Nonce NA|} : set evs |]
           ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"