--- a/src/CTT/CTT.thy Sat Jul 18 20:53:05 2015 +0200
+++ b/src/CTT/CTT.thy Sat Jul 18 20:54:56 2015 +0200
@@ -421,25 +421,25 @@
The (rtac EqE i) lets them apply to equality judgements. **)
fun NE_tac ctxt sp i =
- TRY (rtac @{thm EqE} i) THEN
+ TRY (resolve_tac ctxt @{thms EqE} i) THEN
Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] [] @{thm NE} i
fun SumE_tac ctxt sp i =
- TRY (rtac @{thm EqE} i) THEN
+ TRY (resolve_tac ctxt @{thms EqE} i) THEN
Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] [] @{thm SumE} i
fun PlusE_tac ctxt sp i =
- TRY (rtac @{thm EqE} i) THEN
+ TRY (resolve_tac ctxt @{thms EqE} i) THEN
Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] [] @{thm PlusE} i
(** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **)
(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
fun add_mp_tac ctxt i =
- rtac @{thm subst_prodE} i THEN assume_tac ctxt i THEN assume_tac ctxt i
+ resolve_tac ctxt @{thms subst_prodE} i THEN assume_tac ctxt i THEN assume_tac ctxt i
(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
-fun mp_tac ctxt i = etac @{thm subst_prodE} i THEN assume_tac ctxt i
+fun mp_tac ctxt i = eresolve_tac ctxt @{thms subst_prodE} i THEN assume_tac ctxt i
(*"safe" when regarded as predicate calculus rules*)
val safe_brls = sort (make_ord lessb)