--- a/src/HOL/Auth/Smartcard/Smartcard.thy Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Sun May 18 14:33:01 2025 +0000
@@ -383,8 +383,8 @@
val analz_image_freshK_ss =
simpset_of
- (\<^context> delsimps [image_insert, image_Un]
- delsimps [@{thm imp_disjL}] (*reduces blow-up*)
+ (\<^context> delsimps @{thms image_insert image_Un}
+ delsimps @{thms imp_disjL} (*reduces blow-up*)
addsimps @{thms analz_image_freshK_simps})
end
\<close>
@@ -400,7 +400,7 @@
method_setup analz_freshK = \<open>
Scan.succeed (fn ctxt =>
(SIMPLE_METHOD
- (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
+ (EVERY [REPEAT_FIRST (resolve_tac ctxt @{thms allI ballI impI}),
REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt))])))\<close>
"for proving the Session Key Compromise theorem"