# HG changeset patch
# User wenzelm
# Date 1164769871 -3600
# Node ID a89f786b301a9495ac2303e2a2ebf1b8a94bd6c1
# Parent  3ff126ca39b42c8a2456b23d3d37a68f1cc3a59c
added INCR_COMP, COMP_INCR;

diff -r 3ff126ca39b4 -r a89f786b301a src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Nov 29 04:11:10 2006 +0100
+++ b/src/Pure/drule.ML	Wed Nov 29 04:11:11 2006 +0100
@@ -6,7 +6,7 @@
 Derived rules and other operations on theorems.
 *)
 
-infix 0 RS RSN RL RLN MRS MRL OF COMP;
+infix 0 RS RSN RL RLN MRS MRL OF COMP INCR_COMP COMP_INCR;
 
 signature BASIC_DRULE =
 sig
@@ -53,6 +53,8 @@
   val OF: thm * thm list -> thm
   val compose: thm * int * thm -> thm list
   val COMP: thm * thm -> thm
+  val INCR_COMP: thm * thm -> thm
+  val COMP_INCR: thm * thm -> thm
   val read_instantiate_sg: theory -> (string*string)list -> thm -> thm
   val read_instantiate: (string*string)list -> thm -> thm
   val cterm_instantiate: (cterm*cterm)list -> thm -> thm
@@ -1057,6 +1059,9 @@
 fun incr_indexes2 th1 th2 =
   Thm.incr_indexes (Int.max (Thm.maxidx_of th1, Thm.maxidx_of th2) + 1);
 
+fun th1 INCR_COMP th2 = incr_indexes th2 th1 COMP th2;
+fun th1 COMP_INCR th2 = th1 COMP incr_indexes th1 th2;
+
 
 
 (** multi_resolve **)