src/ZF/pair.thy
changeset 54998 8601434fa334
parent 51717 9e7d1c139569
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/pair.thy	Sun Jan 12 13:16:00 2014 +0100
     1.2 +++ b/src/ZF/pair.thy	Sun Jan 12 14:32:22 2014 +0100
     1.3 @@ -19,17 +19,17 @@
     1.4  ML {* val ZF_ss = simpset_of @{context} *}
     1.5  
     1.6  simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = {*
     1.7 -  let
     1.8 -    val unfold_bex_tac = unfold_tac @{thms Bex_def};
     1.9 -    fun prove_bex_tac ctxt = unfold_bex_tac ctxt THEN Quantifier1.prove_one_point_ex_tac;
    1.10 -  in fn _ => fn ctxt => Quantifier1.rearrange_bex (prove_bex_tac ctxt) ctxt end
    1.11 +  fn _ => Quantifier1.rearrange_bex
    1.12 +    (fn ctxt =>
    1.13 +      unfold_tac ctxt @{thms Bex_def} THEN
    1.14 +      Quantifier1.prove_one_point_ex_tac)
    1.15  *}
    1.16  
    1.17  simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = {*
    1.18 -  let
    1.19 -    val unfold_ball_tac = unfold_tac @{thms Ball_def};
    1.20 -    fun prove_ball_tac ctxt = unfold_ball_tac ctxt THEN Quantifier1.prove_one_point_all_tac;
    1.21 -  in fn _ => fn ctxt => Quantifier1.rearrange_ball (prove_ball_tac ctxt) ctxt end
    1.22 +  fn _ => Quantifier1.rearrange_ball
    1.23 +    (fn ctxt =>
    1.24 +      unfold_tac ctxt @{thms Ball_def} THEN
    1.25 +      Quantifier1.prove_one_point_all_tac)
    1.26  *}
    1.27  
    1.28