src/HOL/Tools/simpdata.ML
changeset 42455 6702c984bf5a
parent 42453 cd5005020f4e
child 42458 5dfae6d348fd
     1.1 --- a/src/HOL/Tools/simpdata.ML	Fri Apr 22 13:07:47 2011 +0200
     1.2 +++ b/src/HOL/Tools/simpdata.ML	Fri Apr 22 13:58:13 2011 +0200
     1.3 @@ -183,14 +183,6 @@
     1.4    let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
     1.5    in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
     1.6  
     1.7 -val defALL_regroup =
     1.8 -  Simplifier.simproc_global @{theory}
     1.9 -    "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
    1.10 -
    1.11 -val defEX_regroup =
    1.12 -  Simplifier.simproc_global @{theory}
    1.13 -    "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
    1.14 -
    1.15  end;
    1.16  
    1.17  structure Splitter = Simpdata.Splitter;