# HG changeset patch
# User paulson
# Date 1146132665 -7200
# Node ID 868cf5051ff568c91c4df992ca9baec513b91d23
# Parent  caaf68a64ac420d73f469aed3a0f027a2a05f540
slight shortening of blacklist

diff -r caaf68a64ac4 -r 868cf5051ff5 src/HOL/Tools/ATP/res_clasimpset.ML
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Apr 27 12:10:47 2006 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Thu Apr 27 12:11:05 2006 +0200
@@ -27,15 +27,7 @@
   FIXME: this blacklist needs to be maintained using theory data and added to using
   an attribute.*)
 val blacklist = ref
-  ["Datatype.not_None_eq",    (*Says everything is None or Some. Probably prolific.*)
-   "Datatype.not_Some_eq_D",  (*Says everything is None or Some. Probably prolific.*)
-   "Datatype.not_Some_eq",    (*Says everything is None or Some. Probably prolific.*)
-   "Datatype.option.size_1",
-   "Datatype.option.size_2",
-   "Datatype.prod.size",
-   "Datatype.sum.size_1",
-   "Datatype.sum.size_2",
-   "Datatype.unit.size",
+  ["Datatype.prod.size",
    "Divides.dvd_0_left_iff",
    "Finite_Set.card_0_eq",
    "Finite_Set.card_infinite",
@@ -53,31 +45,23 @@
    "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", 
    "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
    "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
-   "Infinite_Set.atmost_one_unique",
-   "IntArith.zabs_less_one_iff",
    "IntDef.Integ.Abs_Integ_inject",
    "IntDef.Integ.Abs_Integ_inverse",
    "IntDiv.zdvd_0_left",
-   "IntDiv.zero_less_zpower_abs_iff",
    "List.append_eq_append_conv",
-   "List.Cons_in_lex",
    "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
    "List.in_listsD",
    "List.in_listsI",
    "List.lists.Cons",
    "List.listsE",
-   "List.take_eq_Nil",
-   "Nat.less_one",
    "Nat.less_one", (*not directional? obscure*)
    "Nat.not_gr0",
    "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
    "NatArith.of_nat_0_eq_iff",
    "NatArith.of_nat_eq_0_iff",
    "NatArith.of_nat_le_0_iff",
-   "NatSimprocs.divide_le_0_iff_number_of",  (*seldom used; often prolific*)
    "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
    "NatSimprocs.divide_less_0_iff_number_of",
-   "NatSimprocs.divide_less_0_iff_number_of",   (*too many clauses*)
    "NatSimprocs.equation_minus_iff_1",  (*not directional*)
    "NatSimprocs.equation_minus_iff_number_of", (*not directional*)
    "NatSimprocs.le_minus_iff_1", (*not directional*)
@@ -92,11 +76,8 @@
    "NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*)
    "NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*)
    "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
-   "NatSimprocs.zero_le_divide_iff_number_of",
    "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
    "NatSimprocs.zero_less_divide_iff_number_of",
-   "NatSimprocs.zero_less_divide_iff_number_of", (*excessive case analysis*)
-   "OrderedGroup.abs_0_eq",
    "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
    "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
    "OrderedGroup.join_0_eq_0",
@@ -106,8 +87,6 @@
    "OrderedGroup.pprt_mono",   (*obscure*)
    "Parity.even_nat_power",   (*obscure, somewhat prolilfic*)
    "Parity.power_eq_0_iff_number_of",
-   "Parity.power_eq_0_iff_number_of",
-   "Parity.power_le_zero_eq_number_of",
    "Parity.power_le_zero_eq_number_of",   (*obscure and prolific*)
    "Parity.power_less_zero_eq_number_of",
    "Parity.zero_le_power_eq_number_of",   (*obscure and prolific*)
@@ -123,15 +102,11 @@
    "Ring_and_Field.divide_eq_1_iff",
    "Ring_and_Field.divide_eq_eq_1",
    "Ring_and_Field.divide_le_0_1_iff",
-   "Ring_and_Field.divide_le_eq_1_neg",
    "Ring_and_Field.divide_le_eq_1_neg",  (*obscure and prolific*)
-   "Ring_and_Field.divide_le_eq_1_pos",
    "Ring_and_Field.divide_le_eq_1_pos",  (*obscure and prolific*)
    "Ring_and_Field.divide_less_0_1_iff",
    "Ring_and_Field.divide_less_eq_1_neg",  (*obscure and prolific*)
-   "Ring_and_Field.divide_less_eq_1_pos",
    "Ring_and_Field.divide_less_eq_1_pos",  (*obscure and prolific*)
-   "Ring_and_Field.eq_divide_eq_1",
    "Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*)
    "Ring_and_Field.field_mult_cancel_left",
    "Ring_and_Field.field_mult_cancel_right",
@@ -139,13 +114,9 @@
    "Ring_and_Field.inverse_le_iff_le",
    "Ring_and_Field.inverse_less_iff_less_neg",
    "Ring_and_Field.inverse_less_iff_less",
-   "Ring_and_Field.le_divide_eq_1_neg",
    "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
-   "Ring_and_Field.le_divide_eq_1_pos",
    "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
-   "Ring_and_Field.less_divide_eq_1_neg",
    "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
-   "Ring_and_Field.less_divide_eq_1_pos",
    "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
    "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
    "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
@@ -172,10 +143,8 @@
    "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
    "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
    "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
-   "SetInterval.ivl_subset", (*excessive case analysis*)
-   "Sum_Type.InlI",
-   "Sum_Type.InrI"];
-   
+   "SetInterval.ivl_subset"];  (*excessive case analysis*)
+    
 (*These might be prolific but are probably OK, and min and max are basic.
    "Orderings.max_less_iff_conj", 
    "Orderings.min_less_iff_conj",