changeset 32010 | cb1a1c94b4cd |
parent 31974 | e81979a703a4 |
child 32149 | ef59550a55d3 |
--- a/src/FOL/simpdata.ML Wed Jul 15 23:11:57 2009 +0200 +++ b/src/FOL/simpdata.ML Wed Jul 15 23:48:21 2009 +0200 @@ -85,11 +85,11 @@ end); val defEX_regroup = - Simplifier.simproc (the_context ()) + Simplifier.simproc @{theory} "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex; val defALL_regroup = - Simplifier.simproc (the_context ()) + Simplifier.simproc @{theory} "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;