# HG changeset patch
# User paulson
# Date 1143027224 -3600
# Node ID 3d383e78b6f4872e60a6f9c199d9ed5844cbb525
# Parent  c04b75d482c47ad0fc51ea8e465aca2f74dae977
Introduction of "whitelist": theorems forced past the relevance filter

diff -r c04b75d482c4 -r 3d383e78b6f4 src/HOL/Tools/ATP/res_clasimpset.ML
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Mar 22 12:32:44 2006 +0100
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Mar 22 12:33:44 2006 +0100
@@ -6,6 +6,7 @@
 signature RES_CLASIMP = 
   sig
   val blacklist : string list ref (*Theorems forbidden in the output*)
+  val whitelist : thm list ref    (*Theorems required in the output*)
   val use_simpset: bool ref
   val get_clasimp_atp_lemmas : 
       Proof.context ->
@@ -18,6 +19,8 @@
 struct
 val use_simpset = ref false;   (*Performance is much better without simprules*)
 
+(*The rule subsetI is frequently omitted by the relevance filter.*)
+val whitelist = ref [subsetI]; 
 
 (*In general, these produce clauses that are prolific (match too many equality or
   membership literals) and relate to seldom-used facts. Some duplicate other rules.
@@ -285,7 +288,10 @@
 	      map put_name_pair (ResAxioms.atpset_rules_of_ctxt ctxt)
 	  else []
       val _ = warning_thms atpset_thms
-      val user_rules = map put_name_pair user_thms
+      val user_rules = 
+	  case user_thms of  (*use whitelist if there are no user-supplied rules*)
+	       [] => map (put_name_pair o ResAxioms.pairname) (!whitelist)
+	     | _  => map put_name_pair user_thms
       val banned = make_banned_test (map #1 (user_rules@atpset_thms@claset_thms@simpset_thms))
       fun ok (a,_) = not (banned a) 	   
       val claset_cls_tms =