src/HOL/Auth/OtwayRees_AN.ML
changeset 3451 d10f100676d8
parent 3207 fe79ad367d77
child 3465 e85c24717cad
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Jun 19 11:28:55 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Jun 19 11:31:14 1997 +0200
     1.3 @@ -179,10 +179,9 @@
     1.4  by analz_sees_tac;
     1.5  by (REPEAT_FIRST (resolve_tac [allI, impI]));
     1.6  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
     1.7 -(*14 seconds*)
     1.8  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
     1.9 -(*OR4, Fake*) 
    1.10 -by (EVERY (map spy_analz_tac [3,2]));
    1.11 +(*Fake*) 
    1.12 +by (spy_analz_tac 2);
    1.13  (*Base*)
    1.14  by (Blast_tac 1);
    1.15  qed_spec_mp "analz_image_freshK";
    1.16 @@ -285,16 +284,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,
    1.21 -                                      analz_insert_freshK]
    1.22 +                            addsimps [analz_insert_eq, not_parts_not_analz, 
    1.23 +				      analz_insert_freshK]
    1.24                              setloop split_tac [expand_if])));
    1.25 +(*Oops*)
    1.26 +by (blast_tac (!claset addSDs [unique_session_keys]) 4);
    1.27 +(*OR4*) 
    1.28 +by (Blast_tac 3);
    1.29  (*OR3*)
    1.30  by (blast_tac (!claset addSEs sees_Spy_partsEs
    1.31                         addIs [impOfSubs analz_subset_parts]) 2);
    1.32 -(*Oops*) 
    1.33 -by (blast_tac (!claset addDs [unique_session_keys]) 3);
    1.34 -(*OR4, Fake*) 
    1.35 -by (REPEAT_FIRST spy_analz_tac);
    1.36 +(*Fake*) 
    1.37 +by (spy_analz_tac 1);
    1.38  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    1.39  
    1.40  goal thy