1.1 --- a/src/HOL/Set.thy	Fri Apr 22 13:07:47 2011 +0200
     1.2 +++ b/src/HOL/Set.thy	Fri Apr 22 13:58:13 2011 +0200
     1.3 @@ -75,17 +75,16 @@
     1.4  to the front (and similarly for @{text "t=x"}):
     1.5  *}
     1.6  
     1.7 -setup {*
     1.8 -let
     1.9 -  val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
    1.10 -    ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
    1.11 -                    DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
    1.12 -  val defColl_regroup = Simplifier.simproc_global @{theory}
    1.13 -    "defined Collect" ["{x. P x & Q x}"]
    1.14 -    (Quantifier1.rearrange_Coll Coll_perm_tac)
    1.15 -in
    1.16 -  Simplifier.map_simpset (fn ss => ss addsimprocs [defColl_regroup])
    1.17 -end
    1.18 +simproc_setup defined_Collect ("{x. P x & Q x}") = {*
    1.19 +  let
    1.20 +    val Coll_perm_tac =
    1.21 +      rtac @{thm Collect_cong} 1 THEN
    1.22 +      rtac @{thm iffI} 1 THEN
    1.23 +      ALLGOALS (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]);
    1.24 +  in
    1.25 +    fn _ => fn ss => fn ct =>
    1.26 +      Quantifier1.rearrange_Coll Coll_perm_tac (theory_of_cterm ct) ss (term_of ct)
    1.27 +  end
    1.28  *}
    1.29  
    1.30  lemmas CollectE = CollectD [elim_format]
    1.31 @@ -329,21 +328,24 @@
    1.32    in [(@{const_syntax Collect}, setcompr_tr')] end;
    1.33  *}
    1.34  
    1.35 -setup {*
    1.36 -let
    1.37 -  val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
    1.38 -  fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    1.39 -  val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
    1.40 -  val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
    1.41 -  fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    1.42 -  val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    1.43 -  val defBEX_regroup = Simplifier.simproc_global @{theory}
    1.44 -    "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
    1.45 -  val defBALL_regroup = Simplifier.simproc_global @{theory}
    1.46 -    "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
    1.47 -in
    1.48 -  Simplifier.map_simpset (fn ss => ss addsimprocs [defBALL_regroup, defBEX_regroup])
    1.49 -end
    1.50 +simproc_setup defined_Bex ("EX x:A. P x & Q x") = {*
    1.51 +  let
    1.52 +    val unfold_bex_tac = unfold_tac @{thms Bex_def};
    1.53 +    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    1.54 +  in
    1.55 +    fn _ => fn ss => fn ct =>
    1.56 +      Quantifier1.rearrange_bex prove_bex_tac (theory_of_cterm ct) ss (term_of ct)
    1.57 +  end
    1.58 +*}
    1.59 +
    1.60 +simproc_setup defined_All ("ALL x:A. P x --> Q x") = {*
    1.61 +  let
    1.62 +    val unfold_ball_tac = unfold_tac @{thms Ball_def};
    1.63 +    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    1.64 +  in
    1.65 +    fn _ => fn ss => fn ct =>
    1.66 +      Quantifier1.rearrange_ball prove_ball_tac (theory_of_cterm ct) ss (term_of ct)
    1.67 +  end
    1.68  *}
    1.69  
    1.70  lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"