# HG changeset patch
# User paulson
# Date 1256047368 -3600
# Node ID c95102496490a2176ae33aab986b47304f3e536c
# Parent  c065b9300d441f5795948d5ee01884fabdaa2383
 Removal of the unused atpset concept, the atp attribute and some related code.

diff -r c065b9300d44 -r c95102496490 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Oct 20 15:03:17 2009 +0200
+++ b/src/HOL/HOL.thy	Tue Oct 20 15:02:48 2009 +0100
@@ -839,9 +839,6 @@
 ML_Antiquote.value "claset"
   (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())");
 
-structure ResAtpset = Named_Thms
-  (val name = "atp" val description = "ATP rules");
-
 structure ResBlacklist = Named_Thms
   (val name = "noatp" val description = "theorems blacklisted for ATP");
 *}
@@ -860,7 +857,6 @@
   Hypsubst.hypsubst_setup
   #> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
   #> Classical.setup
-  #> ResAtpset.setup
   #> ResBlacklist.setup
 end
 *}
diff -r c065b9300d44 -r c95102496490 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Oct 20 15:03:17 2009 +0200
+++ b/src/HOL/Set.thy	Tue Oct 20 15:02:48 2009 +0100
@@ -445,7 +445,7 @@
 
 subsubsection {* Subsets *}
 
-lemma subsetI [atp, intro!]: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B"
+lemma subsetI [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B"
   unfolding mem_def by (rule le_funI, rule le_boolI)
 
 text {*
@@ -476,7 +476,7 @@
 lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   by blast
 
-lemma subset_refl [simp,atp]: "A \<subseteq> A"
+lemma subset_refl [simp]: "A \<subseteq> A"
   by (fact order_refl)
 
 lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"
diff -r c065b9300d44 -r c95102496490 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Tue Oct 20 15:03:17 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue Oct 20 15:02:48 2009 +0100
@@ -38,8 +38,6 @@
 val pass_mark = 0.5;
 val convergence = 3.2;    (*Higher numbers allow longer inference chains*)
 val follow_defs = false;  (*Follow definitions. Makes problems bigger.*)
-val include_all = true;
-val include_atpset = true;
   
 (***************************************************************)
 (* Relevance Filtering                                         *)
@@ -293,15 +291,14 @@
 
 (*** white list and black list of lemmas ***)
 
-(*The rule subsetI is frequently omitted by the relevance filter. This could be theory data
-  or identified with ATPset (which however is too big currently)*)
+(*The rule subsetI is frequently omitted by the relevance filter.*)
 val whitelist_fo = [subsetI];
 (* ext has been a 'helper clause', always given to the atps.
   As such it was not passed to metis, but metis does not include ext (in contrast
   to the other helper_clauses *)
 val whitelist_ho = [ResHolClause.ext];
 
-(*** retrieve lemmas from clasimpset and atpset, may filter them ***)
+(*** retrieve lemmas and filter them ***)
 
 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
 
@@ -405,18 +402,11 @@
       (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
   | check_named _ = true;
 
-(* get lemmas from claset, simpset, atpset and extra supplied rules *)
-fun get_clasimp_atp_lemmas ctxt =
+fun get_all_lemmas ctxt =
   let val included_thms =
-    if include_all
-    then (tap (fn ths => ResAxioms.trace_msg
-                 (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
-              (name_thm_pairs ctxt))
-    else
-    let val atpset_thms =
-            if include_atpset then ResAxioms.atpset_rules_of ctxt
-            else []
-    in  atpset_thms  end
+        tap (fn ths => ResAxioms.trace_msg
+                     (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
+            (name_thm_pairs ctxt)
   in
     filter check_named included_thms
   end;
@@ -524,7 +514,7 @@
   let
     val thy = ProofContext.theory_of ctxt
     val isFO = isFO thy goal_cls
-    val included_thms = get_clasimp_atp_lemmas ctxt
+    val included_thms = get_all_lemmas ctxt
     val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
                                      |> restrict_to_logic thy isFO
                                      |> remove_unwanted_clauses
diff -r c065b9300d44 -r c95102496490 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Tue Oct 20 15:03:17 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Tue Oct 20 15:02:48 2009 +0100
@@ -17,7 +17,6 @@
   val expand_defs_tac: thm -> tactic
   val combinators: thm -> thm
   val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list
-  val atpset_rules_of: Proof.context -> (string * thm) list
   val suppress_endtheory: bool Unsynchronized.ref
     (*for emergency use where endtheory causes problems*)
   val setup: theory -> theory
@@ -378,8 +377,6 @@
 
 fun pairname th = (Thm.get_name_hint th, th);
 
-fun atpset_rules_of ctxt = map pairname (ResAtpset.get ctxt);
-
 
 (**** Translate a set of theorems into CNF ****)