src/FOL/simpdata.ML
changeset 42455 6702c984bf5a
parent 42453 cd5005020f4e
child 42458 5dfae6d348fd
     1.1 --- a/src/FOL/simpdata.ML	Fri Apr 22 13:07:47 2011 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Fri Apr 22 13:58:13 2011 +0200
     1.3 @@ -80,14 +80,6 @@
     1.4    val ex_comm = @{thm ex_comm}
     1.5  end);
     1.6  
     1.7 -val defEX_regroup =
     1.8 -  Simplifier.simproc_global @{theory}
     1.9 -    "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
    1.10 -
    1.11 -val defALL_regroup =
    1.12 -  Simplifier.simproc_global @{theory}
    1.13 -    "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
    1.14 -
    1.15  
    1.16  (*** Case splitting ***)
    1.17