src/HOL/Auth/TLS.ML

     etac tls.induct i   THEN
     ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
     ALLGOALS (asm_simp_tac (simpset() addsimps split_ifs @ pushes))  THEN
     (*Remove instances of pubK B:  the Spy already knows all public keys.
       Combining the two simplifier calls makes them run extremely slowly.*)
-    ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]));
+    ALLGOALS (asm_simp_tac (simpset() addsimps [image_eq_UN, insert_absorb]));
 
 
 (*** Properties of items found in Notes ***)
 
 Goal "[| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \

 \  ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
 by (etac rev_mp 1);
 by (hyp_subst_tac 1);
 by (analz_induct_tac 1);
 (*SpyKeys*)
-by (Blast_tac 3);
+by (Blast_tac 2);
 (*Fake*)
-by (blast_tac (claset() addIs [parts_insertI]) 2);
+by (blast_tac (claset() addIs [parts_insertI]) 1);
 (** LEVEL 6 **)
 (*Oops*)
 by (REPEAT 
     (force_tac (claset() addSDs [Notes_Crypt_parts_spies, 
 				 Notes_master_imp_Crypt_PMS],

 \     ==> Key (sessionK((NA,NB,M),role)) ~: parts (spies evs)";
 by (etac rev_mp 1);
 by (etac rev_mp 1);
 by (analz_induct_tac 1);        (*5 seconds*)
 (*SpyKeys*)
-by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 3);
+by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 2);
 (*Fake*) 
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
 qed "sessionK_not_spied";
 
 
 (*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
 Goal "[| evs : tls;  A ~: bad;  B ~: bad |]           \