# HG changeset patch
# User paulson
# Date 1141321843 -3600
# Node ID c6e4b073f6a5aeb0debca24597c9af8eab9fbde8
# Parent  df9de25e87b3845c671e0ab600deee7baf945730
subset_refl now included using the atp attribute

diff -r df9de25e87b3 -r c6e4b073f6a5 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Mar 02 18:49:13 2006 +0100
+++ b/src/HOL/Set.thy	Thu Mar 02 18:50:43 2006 +0100
@@ -522,7 +522,7 @@
 lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   by blast
 
-lemma subset_refl [simp]: "A \<subseteq> A"
+lemma subset_refl [simp,atp]: "A \<subseteq> A"
   by fast
 
 lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"
diff -r df9de25e87b3 -r c6e4b073f6a5 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Mar 02 18:49:13 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Thu Mar 02 18:50:43 2006 +0100
@@ -270,7 +270,7 @@
 (*also works for HOL*) 
 fun skolem_thm th = 
   let val nnfth = to_nnf th
-  in  Meson.make_cnf (skolem_of_nnf nnfth) nnfth
+  in  rm_redundant_cls (Meson.make_cnf (skolem_of_nnf nnfth) nnfth)
   end
   handle THM _ => [];
 
@@ -282,7 +282,7 @@
         (fn nnfth => 
           let val (thy',defs) = declare_skofuns cname nnfth thy
               val skoths = map skolem_of_def defs
-          in (thy', Meson.make_cnf skoths nnfth) end)
+          in (thy', rm_redundant_cls (Meson.make_cnf skoths nnfth)) end)
       (SOME (to_nnf th)  handle THM _ => NONE) 
   end;
 
@@ -346,9 +346,7 @@
 
 fun rules_of_claset cs =
   let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
-      val intros = [subset_refl] @ safeIs @ hazIs
-          (*subset_refl is a special case: obviously useful in resolution, but
-            harmful if added as a default intro rule.*)
+      val intros = safeIs @ hazIs
       val elims  = map Classical.classical_rule (safeEs @ hazEs)
   in
      Output.debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^