src/HOL/Auth/Yahalom.thy

--- a/src/HOL/Auth/Yahalom.thy	Sat Apr 26 12:38:17 2003 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Sat Apr 26 12:38:42 2003 +0200
@@ -150,8 +150,10 @@
  "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