src/HOL/Auth/OtwayRees.ML
changeset 3451 d10f100676d8
parent 3207 fe79ad367d77
child 3465 e85c24717cad
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Jun 19 11:28:55 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Jun 19 11:31:14 1997 +0200
     1.3 @@ -192,10 +192,10 @@
     1.4  by (REPEAT_FIRST (resolve_tac [allI, impI]));
     1.5  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
     1.6  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
     1.7 +(*Fake*) 
     1.8 +by (spy_analz_tac 2);
     1.9  (*Base*)
    1.10  by (Blast_tac 1);
    1.11 -(*Fake, OR2, OR4*) 
    1.12 -by (REPEAT (spy_analz_tac 1));
    1.13  qed_spec_mp "analz_image_freshK";
    1.14  
    1.15  
    1.16 @@ -365,16 +365,18 @@
    1.17  by analz_sees_tac;
    1.18  by (ALLGOALS
    1.19      (asm_simp_tac (!simpset addcongs [conj_cong] 
    1.20 -                            addsimps [not_parts_not_analz, analz_insert_freshK]
    1.21 +                            addsimps [analz_insert_eq, not_parts_not_analz, 
    1.22 +				      analz_insert_freshK]
    1.23                              setloop split_tac [expand_if])));
    1.24 +(*Oops*)
    1.25 +by (blast_tac (!claset addSDs [unique_session_keys]) 4);
    1.26 +(*OR4*) 
    1.27 +by (Blast_tac 3);
    1.28  (*OR3*)
    1.29 -by (blast_tac (!claset delrules [impCE]
    1.30 -                       addSEs sees_Spy_partsEs
    1.31 -                       addIs [impOfSubs analz_subset_parts]) 3);
    1.32 -(*OR4, OR2, Fake*) 
    1.33 -by (REPEAT_FIRST spy_analz_tac);
    1.34 -(*Oops*) (** LEVEL 5 **)
    1.35 -by (blast_tac (!claset addSDs [unique_session_keys]) 1);
    1.36 +by (blast_tac (!claset addSEs sees_Spy_partsEs
    1.37 +                       addIs [impOfSubs analz_subset_parts]) 2);
    1.38 +(*Fake*) 
    1.39 +by (spy_analz_tac 1);
    1.40  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    1.41  
    1.42  goal thy