src/HOL/Tools/res_atp.ML
changeset 20372 e42674e0486e
parent 20289 ba7a7c56bed5
child 20419 df257a9cf0e9
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Aug 09 15:48:51 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Aug 09 18:39:08 2006 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4    val include_all: bool ref
     1.5    val run_relevance_filter: bool ref
     1.6    val run_blacklist_filter: bool ref
     1.7 +  val blacklist: string list ref
     1.8    val add_all : unit -> unit
     1.9    val add_claset : unit -> unit
    1.10    val add_simpset : unit -> unit
    1.11 @@ -304,7 +305,17 @@
    1.12    FIXME: this blacklist needs to be maintained using theory data and added to using
    1.13    an attribute.*)
    1.14  val blacklist = ref
    1.15 -  ["Datatype.prod.size",
    1.16 +  ["Datatype.unit.split_asm",         (*These  "unit" thms cause unsound proofs*)
    1.17 +                               (*Datatype.unit.nchotomy is caught automatically*)
    1.18 +   "Datatype.unit.induct",
    1.19 +   "Datatype.unit.inducts",
    1.20 +   "Datatype.unit.split",
    1.21 +   "Datatype.unit.splits_1",
    1.22 +   "Datatype.unit.splits_2",
    1.23 +   "Product_Type.unit_abs_eta_conv",
    1.24 +   "Product_Type.unit_induct",
    1.25 +
    1.26 +   "Datatype.prod.size",
    1.27     "Divides.dvd_0_left_iff",
    1.28     "Finite_Set.card_0_eq",
    1.29     "Finite_Set.card_infinite",