# HG changeset patch
# User wenzelm
# Date 968352633 -7200
# Node ID be0389a64ce800386aacaada3a7c0a0ac7677e41
# Parent  133c845d2bd1ac90925f8246579a372d530e6625
updated rulify setup;

diff -r 133c845d2bd1 -r be0389a64ce8 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Sep 07 20:50:11 2000 +0200
+++ b/src/HOL/Set.ML	Thu Sep 07 20:50:33 2000 +0200
@@ -779,18 +779,22 @@
 qed "psubset_imp_ex_mem";
 
 
-(* attributes *)
+(* rulify setup *)
+
+Goal "(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)";
+by (simp_tac (simpset () addsimps (Ball_def :: thms "atomize")) 1);
+qed "ball_eq";
 
 local
-
-fun gen_rulify_prems x =
-  Attrib.no_args (Drule.rule_attribute (fn _ => (standard o
-    rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, ballI, impI])))))) x;
-
+  val ss = HOL_basic_ss addsimps
+    (Drule.norm_hhf_eq :: map Thm.symmetric (ball_eq :: thms "atomize"));
 in
 
-val rulify_prems_attrib_setup =
- [Attrib.add_attributes
-  [("rulify_prems", (gen_rulify_prems, gen_rulify_prems), "put theorem into standard rule form")]];
+structure Rulify = RulifyFun
+ (val make_meta = Simplifier.simplify ss
+  val full_make_meta = Simplifier.full_simplify ss);
+
+structure BasicRulify: BASIC_RULIFY = Rulify;
+open BasicRulify;
 
 end;