src/FOL/FOL.thy
changeset 42455 6702c984bf5a
parent 42453 cd5005020f4e
child 42456 13b4b6ba3593
     1.1 --- a/src/FOL/FOL.thy	Fri Apr 22 13:07:47 2011 +0200
     1.2 +++ b/src/FOL/FOL.thy	Fri Apr 22 13:58:13 2011 +0200
     1.3 @@ -305,12 +305,21 @@
     1.4  
     1.5  
     1.6  use "simpdata.ML"
     1.7 +
     1.8 +simproc_setup defined_Ex ("EX x. P(x)") = {*
     1.9 +  fn _ => fn ss => fn ct => Quantifier1.rearrange_ex (theory_of_cterm ct) ss (term_of ct)
    1.10 +*}
    1.11 +
    1.12 +simproc_setup defined_All ("ALL x. P(x)") = {*
    1.13 +  fn _ => fn ss => fn ct => Quantifier1.rearrange_all (theory_of_cterm ct) ss (term_of ct)
    1.14 +*}
    1.15 +
    1.16  ML {*
    1.17  (*intuitionistic simprules only*)
    1.18  val IFOL_ss =
    1.19    FOL_basic_ss
    1.20    addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps})
    1.21 -  addsimprocs [defALL_regroup, defEX_regroup]
    1.22 +  addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}]
    1.23    addcongs [@{thm imp_cong}];
    1.24  
    1.25  (*classical simprules too*)
    1.26 @@ -318,6 +327,7 @@
    1.27  *}
    1.28  
    1.29  setup {* Simplifier.map_simpset (K FOL_ss) *}
    1.30 +
    1.31  setup "Simplifier.method_setup Splitter.split_modifiers"
    1.32  setup Splitter.setup
    1.33  setup clasimp_setup