Added split_rule attribute.
authorberghofe
Wed, 07 Feb 2007 18:01:40 +0100
changeset 22278 70a7cd02fec1
parent 22277 b89dc456dbc6
child 22279 b0d482a9443f
Added split_rule attribute.
src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Wed Feb 07 18:00:38 2007 +0100
+++ b/src/HOL/Tools/split_rule.ML	Wed Feb 07 18:01:40 2007 +0100
@@ -150,7 +150,9 @@
 val setup =
   Attrib.add_attributes
     [("split_format", split_format,
-      "split pair-typed subterms in premises, or function arguments")];
+      "split pair-typed subterms in premises, or function arguments"),
+     ("split_rule", Attrib.no_args (Thm.rule_attribute (K split_rule)),
+      "curries ALL function variables occurring in a rule's conclusion")];
 
 end;