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])
```