--- a/src/Pure/more_thm.ML Thu Oct 28 22:12:08 2010 +0200
+++ b/src/Pure/more_thm.ML Thu Oct 28 22:23:11 2010 +0200
@@ -12,6 +12,7 @@
structure Ctermtab: TABLE
structure Thmtab: TABLE
val aconvc: cterm * cterm -> bool
+ type attribute = Context.generic * thm -> Context.generic * thm
end;
signature THM =
@@ -64,6 +65,7 @@
val close_derivation: thm -> thm
val add_axiom: binding * term -> theory -> (string * thm) * theory
val add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory
+ type attribute = Context.generic * thm -> Context.generic * thm
type binding = binding * attribute list
val empty_binding: binding
val rule_attribute: (Context.generic -> thm -> thm) -> attribute
@@ -382,6 +384,9 @@
(** attributes **)
+(*attributes subsume any kind of rules or context modifiers*)
+type attribute = Context.generic * thm -> Context.generic * thm;
+
type binding = binding * attribute list;
val empty_binding: binding = (Binding.empty, []);