src/ZF/OrdQuant.thy
changeset 18324 d1c4b1112e33
parent 17876 b9c92f384109
child 24893 b8ef7afe3a6b
equal deleted inserted replaced
18323:4365c8d84f69 18324:d1c4b1112e33
   398 text {* Setting up the one-point-rule simproc *}
   398 text {* Setting up the one-point-rule simproc *}
   399 
   399 
   400 ML_setup {*
   400 ML_setup {*
   401 local
   401 local
   402 
   402 
   403 fun prove_rex_tac ss = unfold_tac ss [rex_def] THEN Quantifier1.prove_one_point_ex_tac;
   403 val unfold_rex_tac = unfold_tac [rex_def];
       
   404 fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
   404 val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;
   405 val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;
   405 
   406 
   406 fun prove_rall_tac ss = unfold_tac ss [rall_def] THEN Quantifier1.prove_one_point_all_tac;
   407 val unfold_rall_tac = unfold_tac [rall_def];
       
   408 fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac;
   407 val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;
   409 val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;
   408 
   410 
   409 in
   411 in
   410 
   412 
   411 val defREX_regroup = Simplifier.simproc (the_context ())
   413 val defREX_regroup = Simplifier.simproc (the_context ())