src/HOL/Auth/Event.thy

 lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs
 
 ML
 {*
 fun analz_mono_contra_tac ctxt = 
-  rtac @{thm analz_impI} THEN' 
+  resolve_tac ctxt @{thms analz_impI} THEN' 
   REPEAT1 o (dresolve_tac ctxt @{thms analz_mono_contra})
   THEN' (mp_tac ctxt)
 *}
 
 method_setup analz_mono_contra = {*

 lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))"] for Y evs
 
 ML
 {*
 fun synth_analz_mono_contra_tac ctxt = 
-  rtac @{thm syan_impI} THEN'
+  resolve_tac ctxt @{thms syan_impI} THEN'
   REPEAT1 o 
     (dresolve_tac ctxt
      [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
       @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
       @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])