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.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.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.15  in
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.24  end;