--- a/src/HOL/UNITY/UNITY_tactics.ML Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML Thu Apr 18 17:07:01 2013 +0200
@@ -23,12 +23,13 @@
resolve_tac [@{thm StableI}, @{thm stableI},
@{thm constrains_imp_Constrains}] 1),
(*for safety, the totalize operator can be ignored*)
- simp_tac (HOL_ss addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
+ simp_tac (put_simpset HOL_ss ctxt
+ addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
rtac @{thm constrainsI} 1,
- full_simp_tac (simpset_of ctxt) 1,
+ full_simp_tac ctxt 1,
REPEAT (FIRSTGOAL (etac disjE)),
ALLGOALS (clarify_tac ctxt),
- ALLGOALS (asm_full_simp_tac (simpset_of ctxt))]) i;
+ ALLGOALS (asm_full_simp_tac ctxt)]) i;
(*proves "ensures/leadsTo" properties when the program is specified*)
fun ensures_tac ctxt sact =
@@ -40,22 +41,22 @@
REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
@{thm EnsuresI}, @{thm ensuresI}] 1),
(*now there are two subgoals: co & transient*)
- simp_tac (simpset_of ctxt addsimps [@{thm mk_total_program_def}]) 2,
+ simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
res_inst_tac ctxt
[(("act", 0), sact)] @{thm totalize_transientI} 2
ORELSE res_inst_tac ctxt
[(("act", 0), sact)] @{thm transientI} 2,
(*simplify the command's domain*)
- simp_tac (simpset_of ctxt addsimps @{thms Domain_unfold}) 3,
+ simp_tac (ctxt addsimps @{thms Domain_unfold}) 3,
constrains_tac ctxt 1,
ALLGOALS (clarify_tac ctxt),
- ALLGOALS (asm_lr_simp_tac (simpset_of ctxt))]);
+ ALLGOALS (asm_lr_simp_tac ctxt)]);
(*Composition equivalences, from Lift_prog*)
-fun make_o_equivs th =
- [th,
- th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]),
- th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])];
+fun make_o_equivs ctxt th =
+ [th,
+ th RS @{thm o_equiv_assoc} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_assoc}]),
+ th RS @{thm o_equiv_apply} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_def}, @{thm sub_def}])];