src/CTT/CTT.thy
changeset 27239 f2f42f9fa09d
parent 27208 5fe899199f85
child 35054 a5db9779b026
     1.1 --- a/src/CTT/CTT.thy	Mon Jun 16 17:56:08 2008 +0200
     1.2 +++ b/src/CTT/CTT.thy	Mon Jun 16 22:13:39 2008 +0200
     1.3 @@ -417,13 +417,13 @@
     1.4      The (rtac EqE i) lets them apply to equality judgements. **)
     1.5  
     1.6  fun NE_tac ctxt sp i =
     1.7 -  TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i
     1.8 +  TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i
     1.9  
    1.10  fun SumE_tac ctxt sp i =
    1.11 -  TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i
    1.12 +  TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i
    1.13  
    1.14  fun PlusE_tac ctxt sp i =
    1.15 -  TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i
    1.16 +  TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i
    1.17  
    1.18  (** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
    1.19