src/HOL/Set.thy
changeset 38715 6513ea67d95d
parent 38649 14c207135eff
child 38786 e46e7a9cb622
     1.1 --- a/src/HOL/Set.thy	Wed Aug 25 18:19:04 2010 +0200
     1.2 +++ b/src/HOL/Set.thy	Wed Aug 25 18:36:22 2010 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4    val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
     1.5      ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
     1.6                      DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
     1.7 -  val defColl_regroup = Simplifier.simproc @{theory}
     1.8 +  val defColl_regroup = Simplifier.simproc_global @{theory}
     1.9      "defined Collect" ["{x. P x & Q x}"]
    1.10      (Quantifier1.rearrange_Coll Coll_perm_tac)
    1.11  in
    1.12 @@ -323,9 +323,9 @@
    1.13    val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
    1.14    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    1.15    val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    1.16 -  val defBEX_regroup = Simplifier.simproc @{theory}
    1.17 +  val defBEX_regroup = Simplifier.simproc_global @{theory}
    1.18      "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
    1.19 -  val defBALL_regroup = Simplifier.simproc @{theory}
    1.20 +  val defBALL_regroup = Simplifier.simproc_global @{theory}
    1.21      "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
    1.22  in
    1.23    Simplifier.map_simpset (fn ss => ss addsimprocs [defBALL_regroup, defBEX_regroup])