src/HOL/HOL.ML
changeset 5888 d8e51792ca85
parent 5809 bacf85370ce0
child 6092 d9db67970c73
--- 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;