# HG changeset patch
# User berghofe
# Date 939130186 -7200
# Node ID e7ecfa61744391687041130d1b4713889829453f
# Parent  b0cb304517d49673a166d20c1e29880bc128ff8f
Added attribute rulify_prems (useful for modifying premises of introduction
rules of inductive sets).

diff -r b0cb304517d4 -r e7ecfa617443 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Oct 05 15:29:36 1999 +0200
+++ b/src/HOL/Set.ML	Tue Oct 05 15:29:46 1999 +0200
@@ -745,3 +745,20 @@
 Goal"[| (A::'a set) <= B; B < C|] ==> A < C";
 by (auto_tac (claset(), simpset() addsimps [psubset_eq]));
 qed "subset_psubset_trans";
+
+
+(* attributes *)
+
+local
+
+fun gen_rulify_prems x =
+  Attrib.no_args (Drule.rule_attribute (fn _ => (standard o
+    rule_by_tactic (REPEAT (ALLGOALS (resolve_tac [allI, ballI, impI])))))) x;
+
+in
+
+val rulify_prems_attrib_setup =
+ [Attrib.add_attributes
+  [("rulify_prems", (gen_rulify_prems, gen_rulify_prems), "put theorem into standard rule form")]];
+
+end;
diff -r b0cb304517d4 -r e7ecfa617443 src/HOL/subset.thy
--- a/src/HOL/subset.thy	Tue Oct 05 15:29:36 1999 +0200
+++ b/src/HOL/subset.thy	Tue Oct 05 15:29:46 1999 +0200
@@ -7,4 +7,6 @@
 theory subset = Set
 files "Tools/typedef_package.ML":
 
+setup rulify_prems_attrib_setup
+
 end