--- a/src/CTT/CTT.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/CTT/CTT.thy Fri Mar 20 14:48:04 2015 +0100
@@ -421,13 +421,16 @@
The (rtac EqE i) lets them apply to equality judgements. **)
fun NE_tac ctxt sp i =
- TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm NE} i
+ TRY (rtac @{thm 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 res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm SumE} i
+ TRY (rtac @{thm 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 res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm PlusE} i
+ TRY (rtac @{thm 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. **)