src/HOL/Auth/Smartcard/ShoupRubinBella.thy

  (*Oops2*) dresolve_tac ctxt [@{thm Outpts_A_Card_form_10}] 27 THEN                
  (*Base*)  (force_tac ctxt) 1
 
 fun analz_prepare_tac ctxt = 
          prepare_tac ctxt THEN
-         dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 18 THEN 
- (*SR_U9*) dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 19 THEN 
+         dresolve_tac ctxt @{thms Gets_imp_knows_Spy_analz_Snd} 18 THEN 
+ (*SR_U9*) dresolve_tac ctxt @{thms Gets_imp_knows_Spy_analz_Snd} 19 THEN 
          REPEAT_FIRST (eresolve_tac ctxt [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt)
 
 end
 *}
 

 
 method_setup sc_analz_freshK = {*
     Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
-          REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
+          REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
           ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt
               addsimps [@{thm knows_Spy_Inputs_secureM_srb_Spy},
                   @{thm knows_Spy_Outpts_secureM_srb_Spy},
                   @{thm shouprubin_assumes_securemeans},
                   @{thm analz_image_Key_Un_Nonce}]))]))) *}