# HG changeset patch
# User paulson
# Date 874507060 -7200
# Node ID 8df171ccdbd8e004e3b7057b18323b5c19dcd6ca
# Parent  414e04d7c2d6dc9d0e8a52ac817bbbbef0e75bf3
Fixed comments

diff -r 414e04d7c2d6 -r 8df171ccdbd8 src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Wed Sep 17 16:37:27 1997 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Wed Sep 17 16:37:40 1997 +0200
@@ -276,14 +276,14 @@
                setloop split_tac [expand_if])));
 (*Oops*)
 by (blast_tac (!claset addDs [unique_session_keys]) 5);
-(*NS4*) 
+(*NS3, replay sub-case*) 
 by (Blast_tac 4);
 (*NS2*)
 by (blast_tac (!claset addSEs sees_Spy_partsEs
                        addIs [parts_insertI, impOfSubs analz_subset_parts]) 2);
 (*Fake*) 
 by (spy_analz_tac 1);
-(*NS3*) (**LEVEL 6 **)
+(*NS3, Server sub-case*) (**LEVEL 6 **)
 by (step_tac (!claset delrules [impCE]) 1);
 by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 1);
 by (assume_tac 2);
diff -r 414e04d7c2d6 -r 8df171ccdbd8 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Wed Sep 17 16:37:27 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Wed Sep 17 16:37:40 1997 +0200
@@ -164,7 +164,7 @@
 by (etac yahalom.induct 1);
 by analz_sees_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
-by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
+by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
 (*Fake*) 
 by (spy_analz_tac 2);
@@ -383,14 +383,13 @@
 (*For Oops, simplification proves NBa~=NB.  By Says_Server_KeyWithNonce,
   we get (~ KeyWithNonce K NB evsa); then simplification can apply the
   induction hypothesis with KK = {K}.*)
-by (ALLGOALS  (*22 seconds*)
+by (ALLGOALS  (*17 seconds*)
     (asm_simp_tac 
      (analz_image_freshK_ss addsimps
-        ([all_conj_distrib, analz_image_freshK,
-	  KeyWithNonce_Says, fresh_not_KeyWithNonce, 
-	  imp_disj_not1,  (*Moves NBa~=NB to the front*)
-	  Says_Server_KeyWithNonce] 
-	 @ pushes))));
+        [all_conj_distrib, analz_image_freshK,
+	 KeyWithNonce_Says, fresh_not_KeyWithNonce, 
+	 imp_disj_not1,			      (*Moves NBa~=NB to the front*)
+	 Says_Server_KeyWithNonce])));
 (*Base*)
 by (Blast_tac 1);
 (*Fake*) 
@@ -506,7 +505,7 @@
 by analz_sees_tac;
 by (ALLGOALS
     (asm_simp_tac 
-     (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes)
+     (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
                setloop split_tac [expand_if])));
 (*Prove YM3 by showing that no NB can also be an NA*)
 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]