Added split_rule attribute.
--- 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;