src/ZF/OrdQuant.thy
changeset 17002 fb9261990ffe
parent 16417 9bc16273c2d4
child 17876 b9c92f384109
     1.1 --- a/src/ZF/OrdQuant.thy	Tue Aug 02 19:47:11 2005 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Tue Aug 02 19:47:12 2005 +0200
     1.3 @@ -400,17 +400,17 @@
     1.4  ML_setup {*
     1.5  local
     1.6  
     1.7 -val prove_rex_tac = rewtac rex_def THEN Quantifier1.prove_one_point_ex_tac;
     1.8 +fun prove_rex_tac ss = unfold_tac ss [rex_def] THEN Quantifier1.prove_one_point_ex_tac;
     1.9  val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;
    1.10  
    1.11 -val prove_rall_tac = rewtac rall_def THEN Quantifier1.prove_one_point_all_tac;
    1.12 +fun prove_rall_tac ss = unfold_tac ss [rall_def] THEN Quantifier1.prove_one_point_all_tac;
    1.13  val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;
    1.14  
    1.15  in
    1.16  
    1.17 -val defREX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
    1.18 +val defREX_regroup = Simplifier.simproc (the_context ())
    1.19    "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
    1.20 -val defRALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
    1.21 +val defRALL_regroup = Simplifier.simproc (the_context ())
    1.22    "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
    1.23  
    1.24  end;