--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Sat Jul 18 20:53:05 2015 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Sat Jul 18 20:54:56 2015 +0200
@@ -753,8 +753,8 @@
fun analz_prepare_tac ctxt =
prepare_tac ctxt THEN
- dtac @{thm Gets_imp_knows_Spy_analz_Snd} 18 THEN
- (*SR9*) dtac @{thm Gets_imp_knows_Spy_analz_Snd} 19 THEN
+ dresolve_tac ctxt @{thms Gets_imp_knows_Spy_analz_Snd} 18 THEN
+ (*SR9*) 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
@@ -818,7 +818,7 @@
(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_sr_Spy},
@{thm knows_Spy_Outpts_secureM_sr_Spy},