src/ZF/simpdata.ML
changeset 17002 fb9261990ffe
parent 15570 8d8c70b41bab
child 17325 d9d50222808e
     1.1 --- a/src/ZF/simpdata.ML	Tue Aug 02 19:47:11 2005 +0200
     1.2 +++ b/src/ZF/simpdata.ML	Tue Aug 02 19:47:12 2005 +0200
     1.3 @@ -53,22 +53,20 @@
     1.4    addcongs [if_weak_cong]
     1.5    setSolver type_solver;
     1.6  
     1.7 -
     1.8 -
     1.9  local
    1.10  
    1.11 -val prove_bex_tac = rewtac Bex_def THEN Quantifier1.prove_one_point_ex_tac;
    1.12 +fun prove_bex_tac ss = unfold_tac ss [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;
    1.13  val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
    1.14  
    1.15 -val prove_ball_tac = rewtac Ball_def THEN Quantifier1.prove_one_point_all_tac;
    1.16 +fun prove_ball_tac ss = unfold_tac ss [Ball_def] THEN Quantifier1.prove_one_point_all_tac;
    1.17  val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    1.18  
    1.19  in
    1.20  
    1.21 -val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
    1.22 +val defBEX_regroup = Simplifier.simproc (the_context ())
    1.23    "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
    1.24  
    1.25 -val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
    1.26 +val defBALL_regroup = Simplifier.simproc (the_context ())
    1.27    "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
    1.28  
    1.29  end;