src/HOL/Auth/Shared.thy

--- a/src/HOL/Auth/Shared.thy	Wed Apr 09 12:51:49 2003 +0200
+++ b/src/HOL/Auth/Shared.thy	Wed Apr 09 12:52:45 2003 +0200
@@ -46,7 +46,7 @@
 method_setup analz_freshK = {*
     Method.no_args
      (Method.METHOD
-      (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, impI]),
+      (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
                           REPEAT_FIRST (rtac analz_image_freshK_lemma),
                           ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *}
     "for proving the Session Key Compromise theorem"