Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Auth/Smartcard/ShoupRubin.thy
changeset 82630 2bb4a8d0111d
parent 80914 d97fdabd9e2b 
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Fri May 16 20:44:51 2025 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Sun May 18 14:33:01 2025 +0000
@@ -817,7 +817,7 @@
     Scan.succeed (fn ctxt =>
      (SIMPLE_METHOD
       (EVERY [REPEAT_FIRST
-       (resolve_tac ctxt [allI, ballI, impI]),
+       (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
           addsimps [@{thm knows_Spy_Inputs_secureM_sr_Spy},
isabelle