src/HOL/Tools/ATP/res_clasimpset.ML
changeset 18985 bc23b1d1ddea
parent 18869 00741f7280f7
child 19010 fef9e4881e83
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Feb 09 12:14:39 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Feb 09 12:20:02 2006 +0100
     1.3 @@ -23,9 +23,9 @@
     1.4    FIXME: this blacklist needs to be maintained using theory data and added to using
     1.5    an attribute.*)
     1.6  val blacklist = ref
     1.7 -  ["Datatype.not_None_eq_iff2",
     1.8 -   "Datatype.not_Some_eq_D",
     1.9 -   "Datatype.not_Some_eq",
    1.10 +  ["Datatype.not_None_eq",    (*Says everything is None or Some. Probably prolific.*)
    1.11 +   "Datatype.not_Some_eq_D",  (*Says everything is None or Some. Probably prolific.*)
    1.12 +   "Datatype.not_Some_eq",    (*Says everything is None or Some. Probably prolific.*)
    1.13     "Datatype.option.size_1",
    1.14     "Datatype.option.size_2",
    1.15     "Datatype.prod.size",
    1.16 @@ -57,6 +57,7 @@
    1.17     "IntDiv.zero_less_zpower_abs_iff",
    1.18     "List.append_eq_append_conv",
    1.19     "List.Cons_in_lex",
    1.20 +   "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
    1.21     "List.in_listsD",
    1.22     "List.in_listsI",
    1.23     "List.lists.Cons",