--- a/src/CTT/CTT.thy Mon Jun 16 17:56:08 2008 +0200
+++ b/src/CTT/CTT.thy Mon Jun 16 22:13:39 2008 +0200
@@ -417,13 +417,13 @@
The (rtac EqE i) lets them apply to equality judgements. **)
fun NE_tac ctxt sp i =
- TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i
+ TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i
fun SumE_tac ctxt sp i =
- TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i
+ TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i
fun PlusE_tac ctxt sp i =
- TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i
+ TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i
(** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **)