subset_refl now included using the atp attribute
authorpaulson
Thu Mar 02 18:50:43 2006 +0100 (2006-03-02)
changeset 19175c6e4b073f6a5
parent 19174 df9de25e87b3
child 19176 52b6ecd0433a
subset_refl now included using the atp attribute
src/HOL/Set.thy
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Set.thy	Thu Mar 02 18:49:13 2006 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Mar 02 18:50:43 2006 +0100
     1.3 @@ -522,7 +522,7 @@
     1.4  lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
     1.5    by blast
     1.6  
     1.7 -lemma subset_refl [simp]: "A \<subseteq> A"
     1.8 +lemma subset_refl [simp,atp]: "A \<subseteq> A"
     1.9    by fast
    1.10  
    1.11  lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Mar 02 18:49:13 2006 +0100
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Mar 02 18:50:43 2006 +0100
     2.3 @@ -270,7 +270,7 @@
     2.4  (*also works for HOL*) 
     2.5  fun skolem_thm th = 
     2.6    let val nnfth = to_nnf th
     2.7 -  in  Meson.make_cnf (skolem_of_nnf nnfth) nnfth
     2.8 +  in  rm_redundant_cls (Meson.make_cnf (skolem_of_nnf nnfth) nnfth)
     2.9    end
    2.10    handle THM _ => [];
    2.11  
    2.12 @@ -282,7 +282,7 @@
    2.13          (fn nnfth => 
    2.14            let val (thy',defs) = declare_skofuns cname nnfth thy
    2.15                val skoths = map skolem_of_def defs
    2.16 -          in (thy', Meson.make_cnf skoths nnfth) end)
    2.17 +          in (thy', rm_redundant_cls (Meson.make_cnf skoths nnfth)) end)
    2.18        (SOME (to_nnf th)  handle THM _ => NONE) 
    2.19    end;
    2.20  
    2.21 @@ -346,9 +346,7 @@
    2.22  
    2.23  fun rules_of_claset cs =
    2.24    let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
    2.25 -      val intros = [subset_refl] @ safeIs @ hazIs
    2.26 -          (*subset_refl is a special case: obviously useful in resolution, but
    2.27 -            harmful if added as a default intro rule.*)
    2.28 +      val intros = safeIs @ hazIs
    2.29        val elims  = map Classical.classical_rule (safeEs @ hazEs)
    2.30    in
    2.31       Output.debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^