src/HOL/Set.thy
changeset 32010 cb1a1c94b4cd
parent 31991 37390299214a
child 32075 e8e0fb5da77a
     1.1 --- a/src/HOL/Set.thy	Wed Jul 15 23:11:57 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Wed Jul 15 23:48:21 2009 +0200
     1.3 @@ -478,9 +478,9 @@
     1.4      fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
     1.5      val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
     1.6    in
     1.7 -    val defBEX_regroup = Simplifier.simproc (the_context ())
     1.8 +    val defBEX_regroup = Simplifier.simproc @{theory}
     1.9        "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
    1.10 -    val defBALL_regroup = Simplifier.simproc (the_context ())
    1.11 +    val defBALL_regroup = Simplifier.simproc @{theory}
    1.12        "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
    1.13    end;
    1.14  
    1.15 @@ -1014,7 +1014,7 @@
    1.16      ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
    1.17                      DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
    1.18    in
    1.19 -    val defColl_regroup = Simplifier.simproc (the_context ())
    1.20 +    val defColl_regroup = Simplifier.simproc @{theory}
    1.21        "defined Collect" ["{x. P x & Q x}"]
    1.22        (Quantifier1.rearrange_Coll Coll_perm_tac)
    1.23    end;