--- a/src/HOL/Auth/Shared.thy Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Auth/Shared.thy Thu Apr 18 17:07:01 2013 +0200
@@ -200,7 +200,7 @@
such as Nonce ?N \<notin> used evs that match Nonce_supply*)
fun possibility_tac ctxt =
(REPEAT
- (ALLGOALS (simp_tac (simpset_of ctxt
+ (ALLGOALS (simp_tac (ctxt
delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets}]
setSolver safe_solver))
THEN
@@ -211,15 +211,16 @@
nonces and keys initially*)
fun basic_possibility_tac ctxt =
REPEAT
- (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver))
+ (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
THEN
REPEAT_FIRST (resolve_tac [refl, conjI]))
val analz_image_freshK_ss =
- @{simpset} delsimps [image_insert, image_Un]
+ simpset_of
+ (@{context} delsimps [image_insert, image_Un]
delsimps [@{thm imp_disjL}] (*reduces blow-up*)
- addsimps @{thms analz_image_freshK_simps}
+ addsimps @{thms analz_image_freshK_simps})
end
*}
@@ -238,7 +239,7 @@
(SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
- ALLGOALS (asm_simp_tac (Simplifier.context ctxt Shared.analz_image_freshK_ss))]))) *}
+ ALLGOALS (asm_simp_tac (put_simpset Shared.analz_image_freshK_ss ctxt))]))) *}
"for proving the Session Key Compromise theorem"
method_setup possibility = {*