src/ZF/OrdQuant.thy
changeset 18324 d1c4b1112e33
parent 17876 b9c92f384109
child 24893 b8ef7afe3a6b
     1.1 --- a/src/ZF/OrdQuant.thy	Thu Dec 01 18:45:24 2005 +0100
     1.2 +++ b/src/ZF/OrdQuant.thy	Thu Dec 01 22:03:01 2005 +0100
     1.3 @@ -400,10 +400,12 @@
     1.4  ML_setup {*
     1.5  local
     1.6  
     1.7 -fun prove_rex_tac ss = unfold_tac ss [rex_def] THEN Quantifier1.prove_one_point_ex_tac;
     1.8 +val unfold_rex_tac = unfold_tac [rex_def];
     1.9 +fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    1.10  val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;
    1.11  
    1.12 -fun prove_rall_tac ss = unfold_tac ss [rall_def] THEN Quantifier1.prove_one_point_all_tac;
    1.13 +val unfold_rall_tac = unfold_tac [rall_def];
    1.14 +fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac;
    1.15  val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;
    1.16  
    1.17  in