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