src/HOL/Auth/Yahalom.thy
changeset 38795 848be46708dc
parent 37936 1e4c5015a72e
child 45605 a89b4bc311a5
--- a/src/HOL/Auth/Yahalom.thy	Fri Aug 27 10:55:20 2010 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Fri Aug 27 10:56:46 2010 +0200
@@ -197,6 +197,7 @@
 apply (erule yahalom.induct,
        drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
 apply (simp only: Says_Server_not_range analz_image_freshK_simps)
+apply safe
 done
 
 lemma analz_insert_freshK: