| changeset 26499 | b4db4e165758 |
| parent 24893 | b8ef7afe3a6b |
| child 32952 | aeb1e44fbc19 |
--- a/src/ZF/simpdata.ML Sat Mar 29 22:56:00 2008 +0100 +++ b/src/ZF/simpdata.ML Sat Mar 29 22:56:01 2008 +0100 @@ -61,10 +61,10 @@ in -val defBEX_regroup = Simplifier.simproc @{theory} +val defBEX_regroup = Simplifier.simproc (Theory.deref @{theory_ref}) "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex; -val defBALL_regroup = Simplifier.simproc @{theory} +val defBALL_regroup = Simplifier.simproc (Theory.deref @{theory_ref}) "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball; end;