# HG changeset patch
# User paulson
# Date 869563562 -7200
# Node ID 82f33248d89d119296e201f532e13bbb05065dba
# Parent  db5e9aceea49d6b624e69a05d238509af758c118
Cosmetic changes: margins, indentation, ...

diff -r db5e9aceea49 -r 82f33248d89d src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Tue Jul 22 11:23:03 1997 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Tue Jul 22 11:26:02 1997 +0200
@@ -209,10 +209,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";
@@ -277,8 +275,8 @@
 (*Crucial property: If the encrypted message appears, and A has used NA
   to start a run, then it originated with the Server!*)
 goal thy 
- "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                 \
-\    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs)      \
+ "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                      \
+\    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs)           \
 \        --> Says A B {|NA, Agent A, Agent B,                          \
 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
 \             : set evs -->                                            \
@@ -295,8 +293,8 @@
 (*OR4*)
 by (REPEAT (Safe_step_tac 2));
 by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
-by (fast_tac (!claset addSIs [Crypt_imp_OR1]
-                      addEs  sees_Spy_partsEs) 2);
+by (blast_tac (!claset addSIs [Crypt_imp_OR1]
+                       addEs  sees_Spy_partsEs) 2);
 (*OR3*)  (** LEVEL 5 **)
 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
 by (step_tac (!claset delrules [disjCI, impCE]) 1);
diff -r db5e9aceea49 -r 82f33248d89d src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Jul 22 11:23:03 1997 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Jul 22 11:26:02 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 |]                               \
-\        ==> EX K. EX NA. EX evs: otway.                                 \
+\        ==> EX K. EX NA. EX evs: otway.                                      \
 \             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
 \             : set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
@@ -125,7 +125,7 @@
 \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
 \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
 \             : set evs;                                            \
-\           evs : otway |]                                     \
+\           evs : otway |]                                          \
 \        ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
 by (etac rev_mp 1);
 by (etac otway.induct 1);
@@ -183,9 +183,9 @@
 (*** The Key K uniquely identifies the Server's  message. **)
 
 goal thy 
- "!!evs. evs : otway ==>                                   \
-\      EX A' B' NA' NB'. ALL A B NA NB.                    \
-\       Says Server B                                      \
+ "!!evs. evs : otway ==>                                            \
+\      EX A' B' NA' NB'. ALL A B NA NB.                             \
+\       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'";
@@ -258,12 +258,12 @@
     the premises, e.g. by having A=Spy **)
 
 goal thy 
- "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                         \
-\        ==> 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 -->                   \
+ "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                 \
+\        ==> 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 -->           \
 \            Key K ~: analz (sees Spy evs)";
 by (etac otway.induct 1);
 by analz_sees_tac;
diff -r db5e9aceea49 -r 82f33248d89d src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Tue Jul 22 11:23:03 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Tue Jul 22 11:26:02 1997 +0200
@@ -278,8 +278,8 @@
 (*B knows, by the first part of A's message, that the Server distributed 
   the key for A and B.  But this part says nothing about nonces.*)
 goal thy 
- "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees Spy evs); \
-\           B ~: lost;  evs : yahalom |]                           \
+ "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees Spy evs);   \
+\           B ~: lost;  evs : yahalom |]                                \
 \        ==> EX NA NB. Says Server A                                    \
 \                        {|Crypt (shrK A) {|Agent B, Key K,             \
 \                                           Nonce NA, Nonce NB|},       \
@@ -299,10 +299,10 @@
  "!!evs. evs : yahalom                                             \
 \        ==> Nonce NB ~: analz (sees Spy evs) -->                  \
 \            Crypt K (Nonce NB) : parts (sees Spy evs) -->         \
-\            (EX A B NA. Says Server A                                  \
-\                        {|Crypt (shrK A) {|Agent B, Key K,             \
-\                                  Nonce NA, Nonce NB|},                \
-\                          Crypt (shrK B) {|Agent A, Key K|}|}          \
+\            (EX A B NA. Says Server A                             \
+\                        {|Crypt (shrK A) {|Agent B, Key K,        \
+\                                  Nonce NA, Nonce NB|},           \
+\                          Crypt (shrK B) {|Agent A, Key K|}|}     \
 \                       : set evs)";
 by (parts_induct_tac 1);
 (*YM3 & Fake*)