--- a/src/FOL/IFOL.ML Mon Nov 16 11:11:42 1998 +0100
+++ b/src/FOL/IFOL.ML Mon Nov 16 11:11:58 1998 +0100
@@ -441,3 +441,18 @@
bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
end;
+
+
+(* attributes *)
+
+local
+
+fun gen_rulify x = Attrib.no_args (Attribute.rule (K (normalize_thm [RSspec, RSmp]))) x;
+
+in
+
+val attrib_setup =
+ [Attrib.add_attributes
+ [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
+
+end;
--- a/src/HOL/HOL.ML Mon Nov 16 11:11:42 1998 +0100
+++ b/src/HOL/HOL.ML Mon Nov 16 11:11:58 1998 +0100
@@ -416,3 +416,18 @@
bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
end;
+
+
+(* attributes *)
+
+local
+
+fun gen_rulify x = Attrib.no_args (Attribute.rule (K (normalize_thm [RSspec, RSmp]))) x;
+
+in
+
+val attrib_setup =
+ [Attrib.add_attributes
+ [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
+
+end;