src/FOL/IFOL.ML

--- 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;