src/HOL/Set.thy
 changeset 18328 841261f303a1 parent 18315 e52f867ab851 child 18413 50c0c118e96d
```     1.1 --- a/src/HOL/Set.thy	Thu Dec 01 22:03:06 2005 +0100
1.2 +++ b/src/HOL/Set.thy	Thu Dec 01 22:04:27 2005 +0100
1.3 @@ -426,24 +426,17 @@
1.4
1.5  ML_setup {*
1.6    local
1.7 -    val Ball_def = thm "Ball_def";
1.8 -    val Bex_def = thm "Bex_def";
1.9 -
1.10 -    val simpset = Simplifier.clear_ss HOL_basic_ss;
1.11 -    fun unfold_tac ss th =
1.12 -      ALLGOALS (full_simp_tac (Simplifier.inherit_context ss simpset addsimps [th]));
1.13 -
1.14 -    fun prove_bex_tac ss =
1.15 -      unfold_tac ss Bex_def THEN Quantifier1.prove_one_point_ex_tac;
1.16 +    val unfold_bex_tac = unfold_tac [thm "Bex_def"];
1.17 +    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
1.18      val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
1.19
1.20 -    fun prove_ball_tac ss =
1.21 -      unfold_tac ss Ball_def THEN Quantifier1.prove_one_point_all_tac;
1.22 +    val unfold_ball_tac = unfold_tac [thm "Ball_def"];
1.23 +    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
1.24      val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
1.25    in
1.26 -    val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
1.27 +    val defBEX_regroup = Simplifier.simproc (the_context ())
1.28        "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
1.29 -    val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
1.30 +    val defBALL_regroup = Simplifier.simproc (the_context ())
1.31        "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
1.32    end;
1.33
```