src/HOL/Auth/Yahalom.thy

 (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
 lemma new_keys_not_used [rule_format, simp]:
  "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
 apply (erule yahalom.induct, force, 
        frule_tac [6] YM4_parts_knows_Spy, simp_all)
-(*Fake, YM3, YM4*)
-apply (blast dest!: keysFor_parts_insert)+
+txt{*Fake*}
+apply (force dest!: keysFor_parts_insert)
+txt{*YM3, YM4*}
+apply blast+
 done
 
 
 (*Earlier, all protocol proofs declared this theorem.  
   But only a few proofs need it, e.g. Yahalom and Kerberos IV.*)