# HG changeset patch
# User wenzelm
# Date 928518837 -7200
# Node ID 111845fce1b741c0afbd441a52e0c97b316013b1
# Parent  951d5f5c3c9515f2bd894b821691afbfe6f523d8
added COMP attribute;

diff -r 951d5f5c3c95 -r 111845fce1b7 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Jun 04 19:53:27 1999 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Jun 04 19:53:57 1999 +0200
@@ -164,6 +164,15 @@
 val local_transfer = gen_transfer ProofContext.theory_of;
 
 
+(* COMP *)
+
+fun comp B (x, A) = (x, A COMP B);
+
+fun gen_COMP thm = syntax (thm >> comp);
+val global_COMP = gen_COMP global_thm;
+val local_COMP = gen_COMP local_thm;
+
+
 (* RS *)
 
 fun resolve (i, B) (x, A) = (x, A RSN (i, B));
@@ -250,6 +259,7 @@
 val pure_attributes =
  [("tag", (gen_tag, gen_tag), "tag theorem"),
   ("untag", (gen_untag, gen_untag), "untag theorem"),
+  ("COMP", (global_COMP, local_COMP), "compose rules (no lifting)"),
   ("RS", (global_RS, local_RS), "resolve with rule"),
   ("APP", (global_APP, local_APP), "resolve rule with"),
   ("where", (global_where, local_where), "named instantiation of theorem"),