--- a/src/HOL/UNITY/UNITY_tactics.ML Sat Jul 18 20:53:05 2015 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML Sat Jul 18 20:54:56 2015 +0200
@@ -7,7 +7,9 @@
(*Combines two invariance ASSUMPTIONS into one. USEFUL??*)
fun Always_Int_tac ctxt =
- dtac @{thm Always_Int_I} THEN' assume_tac ctxt THEN' etac @{thm Always_thin}
+ dresolve_tac ctxt @{thms Always_Int_I} THEN'
+ assume_tac ctxt THEN'
+ eresolve_tac ctxt @{thms Always_thin}
(*Combines a list of invariance THEOREMS into one.*)
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
@@ -19,16 +21,16 @@
(EVERY
[REPEAT (Always_Int_tac ctxt 1),
(*reduce the fancy safety properties to "constrains"*)
- REPEAT (etac @{thm Always_ConstrainsI} 1
+ REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1
ORELSE
resolve_tac ctxt [@{thm StableI}, @{thm stableI},
@{thm constrains_imp_Constrains}] 1),
(*for safety, the totalize operator can be ignored*)
simp_tac (put_simpset HOL_ss ctxt
addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
- rtac @{thm constrainsI} 1,
+ resolve_tac ctxt @{thms constrainsI} 1,
full_simp_tac ctxt 1,
- REPEAT (FIRSTGOAL (etac disjE)),
+ REPEAT (FIRSTGOAL (eresolve_tac ctxt [disjE])),
ALLGOALS (clarify_tac ctxt),
ALLGOALS (asm_full_simp_tac ctxt)]) i;
@@ -37,7 +39,7 @@
SELECT_GOAL
(EVERY
[REPEAT (Always_Int_tac ctxt 1),
- etac @{thm Always_LeadsTo_Basis} 1
+ eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
@{thm EnsuresI}, @{thm ensuresI}] 1),