src/HOL/Tools/Meson/meson.ML
changeset 43264 a1a48c69d623
parent 42833 c0abc218b8b4
child 43821 048619bb1dc3
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Wed Jun 08 08:47:43 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Wed Jun 08 08:47:43 2011 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
     1.5    val finish_cnf: thm list -> thm list
     1.6    val unfold_set_const_simps : Proof.context -> thm list
     1.7 +  val presimplified_consts : Proof.context -> string list
     1.8    val presimplify: Proof.context -> thm -> thm
     1.9    val make_nnf: Proof.context -> thm -> thm
    1.10    val choice_theorems : theory -> thm list
    1.11 @@ -576,7 +577,15 @@
    1.12  
    1.13  val nnf_ss =
    1.14    HOL_basic_ss addsimps nnf_extra_simps
    1.15 -    addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq}, @{simproc let_simp}];
    1.16 +    addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
    1.17 +                 @{simproc let_simp}]
    1.18 +
    1.19 +fun presimplified_consts ctxt =
    1.20 +  [@{const_name simp_implies}, @{const_name False}, @{const_name True},
    1.21 +   @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}, @{const_name If},
    1.22 +   @{const_name Let}]
    1.23 +  |> Config.get ctxt unfold_set_consts
    1.24 +     ? append ([@{const_name Collect}, @{const_name Set.member}])
    1.25  
    1.26  fun presimplify ctxt =
    1.27    rewrite_rule (map safe_mk_meta_eq nnf_simps)