Fixed comments
authorpaulson
Wed Sep 17 16:37:40 1997 +0200 (1997-09-17)
changeset 36798df171ccdbd8
parent 3678 414e04d7c2d6
child 3680 7588653475b2
Fixed comments
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/Yahalom.ML
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Wed Sep 17 16:37:27 1997 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Wed Sep 17 16:37:40 1997 +0200
     1.3 @@ -276,14 +276,14 @@
     1.4                 setloop split_tac [expand_if])));
     1.5  (*Oops*)
     1.6  by (blast_tac (!claset addDs [unique_session_keys]) 5);
     1.7 -(*NS4*) 
     1.8 +(*NS3, replay sub-case*) 
     1.9  by (Blast_tac 4);
    1.10  (*NS2*)
    1.11  by (blast_tac (!claset addSEs sees_Spy_partsEs
    1.12                         addIs [parts_insertI, impOfSubs analz_subset_parts]) 2);
    1.13  (*Fake*) 
    1.14  by (spy_analz_tac 1);
    1.15 -(*NS3*) (**LEVEL 6 **)
    1.16 +(*NS3, Server sub-case*) (**LEVEL 6 **)
    1.17  by (step_tac (!claset delrules [impCE]) 1);
    1.18  by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 1);
    1.19  by (assume_tac 2);
     2.1 --- a/src/HOL/Auth/Yahalom.ML	Wed Sep 17 16:37:27 1997 +0200
     2.2 +++ b/src/HOL/Auth/Yahalom.ML	Wed Sep 17 16:37:40 1997 +0200
     2.3 @@ -164,7 +164,7 @@
     2.4  by (etac yahalom.induct 1);
     2.5  by analz_sees_tac;
     2.6  by (REPEAT_FIRST (resolve_tac [allI, impI]));
     2.7 -by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
     2.8 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
     2.9  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
    2.10  (*Fake*) 
    2.11  by (spy_analz_tac 2);
    2.12 @@ -383,14 +383,13 @@
    2.13  (*For Oops, simplification proves NBa~=NB.  By Says_Server_KeyWithNonce,
    2.14    we get (~ KeyWithNonce K NB evsa); then simplification can apply the
    2.15    induction hypothesis with KK = {K}.*)
    2.16 -by (ALLGOALS  (*22 seconds*)
    2.17 +by (ALLGOALS  (*17 seconds*)
    2.18      (asm_simp_tac 
    2.19       (analz_image_freshK_ss addsimps
    2.20 -        ([all_conj_distrib, analz_image_freshK,
    2.21 -	  KeyWithNonce_Says, fresh_not_KeyWithNonce, 
    2.22 -	  imp_disj_not1,  (*Moves NBa~=NB to the front*)
    2.23 -	  Says_Server_KeyWithNonce] 
    2.24 -	 @ pushes))));
    2.25 +        [all_conj_distrib, analz_image_freshK,
    2.26 +	 KeyWithNonce_Says, fresh_not_KeyWithNonce, 
    2.27 +	 imp_disj_not1,			      (*Moves NBa~=NB to the front*)
    2.28 +	 Says_Server_KeyWithNonce])));
    2.29  (*Base*)
    2.30  by (Blast_tac 1);
    2.31  (*Fake*) 
    2.32 @@ -506,7 +505,7 @@
    2.33  by analz_sees_tac;
    2.34  by (ALLGOALS
    2.35      (asm_simp_tac 
    2.36 -     (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes)
    2.37 +     (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
    2.38                 setloop split_tac [expand_if])));
    2.39  (*Prove YM3 by showing that no NB can also be an NA*)
    2.40  by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]