improved atomize setup;
authorwenzelm
Sun Oct 14 20:10:44 2001 +0200 (2001-10-14)
changeset 117665200b3a8f6e3
parent 11765 4c45eb23ef68
child 11767 7380c9d45626
improved atomize setup;
src/ZF/ZF.ML
     1.1 --- a/src/ZF/ZF.ML	Sun Oct 14 20:09:59 2001 +0200
     1.2 +++ b/src/ZF/ZF.ML	Sun Oct 14 20:10:44 2001 +0200
     1.3 @@ -514,12 +514,12 @@
     1.4  (* update rulify setup -- include bounded All *)
     1.5  
     1.6  Goal "(!!x. x:A ==> P(x)) == Trueprop (ALL x:A. P(x))";
     1.7 -by (simp_tac (simpset () addsimps (Ball_def :: thms "atomize")) 1);
     1.8 -qed "ball_eq";
     1.9 +by (simp_tac (simpset () addsimps [Ball_def, thm "atomize_all", thm "atomize_imp"]) 1);
    1.10 +qed "atomize_ball";
    1.11  
    1.12  local
    1.13    val ss = FOL_basic_ss addsimps
    1.14 -    (Drule.norm_hhf_eq :: map Thm.symmetric (ball_eq :: thms "atomize"));
    1.15 +    [Drule.norm_hhf_eq, Thm.symmetric atomize_ball, Thm.symmetric (thm "atomize_all"), Thm.symmetric (thm "atomize_imp")];
    1.16  in
    1.17  
    1.18  structure Rulify = RulifyFun