updated rulify setup;
authorwenzelm
Thu Sep 07 20:50:33 2000 +0200 (2000-09-07)
changeset 9892be0389a64ce8
parent 9891 133c845d2bd1
child 9893 93d2fde0306c
updated rulify setup;
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Thu Sep 07 20:50:11 2000 +0200
     1.2 +++ b/src/HOL/Set.ML	Thu Sep 07 20:50:33 2000 +0200
     1.3 @@ -779,18 +779,22 @@
     1.4  qed "psubset_imp_ex_mem";
     1.5  
     1.6  
     1.7 -(* attributes *)
     1.8 +(* rulify setup *)
     1.9 +
    1.10 +Goal "(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)";
    1.11 +by (simp_tac (simpset () addsimps (Ball_def :: thms "atomize")) 1);
    1.12 +qed "ball_eq";
    1.13  
    1.14  local
    1.15 -
    1.16 -fun gen_rulify_prems x =
    1.17 -  Attrib.no_args (Drule.rule_attribute (fn _ => (standard o
    1.18 -    rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, ballI, impI])))))) x;
    1.19 -
    1.20 +  val ss = HOL_basic_ss addsimps
    1.21 +    (Drule.norm_hhf_eq :: map Thm.symmetric (ball_eq :: thms "atomize"));
    1.22  in
    1.23  
    1.24 -val rulify_prems_attrib_setup =
    1.25 - [Attrib.add_attributes
    1.26 -  [("rulify_prems", (gen_rulify_prems, gen_rulify_prems), "put theorem into standard rule form")]];
    1.27 +structure Rulify = RulifyFun
    1.28 + (val make_meta = Simplifier.simplify ss
    1.29 +  val full_make_meta = Simplifier.full_simplify ss);
    1.30 +
    1.31 +structure BasicRulify: BASIC_RULIFY = Rulify;
    1.32 +open BasicRulify;
    1.33  
    1.34  end;