removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;
authorwenzelm
Thu Mar 05 21:06:59 2009 +0100 (2009-03-05)
changeset 30291a1c3abf57068
parent 30290 f49d70426690
child 30292 a3bb22493f11
removed obsolete claset_rules_of, simpset_rules_of -- as proposed in the text;
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Mar 05 20:55:28 2009 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Mar 05 21:06:59 2009 +0100
     1.3 @@ -34,8 +34,6 @@
     1.4  val convergence = 3.2;    (*Higher numbers allow longer inference chains*)
     1.5  val follow_defs = false;  (*Follow definitions. Makes problems bigger.*)
     1.6  val include_all = true;
     1.7 -val include_simpset = false;
     1.8 -val include_claset = false;
     1.9  val include_atpset = true;
    1.10    
    1.11  (***************************************************************)
    1.12 @@ -409,17 +407,11 @@
    1.13                       (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
    1.14                    (name_thm_pairs ctxt))
    1.15          else
    1.16 -        let val claset_thms =
    1.17 -                if include_claset then ResAxioms.claset_rules_of ctxt
    1.18 -                else []
    1.19 -            val simpset_thms =
    1.20 -                if include_simpset then ResAxioms.simpset_rules_of ctxt
    1.21 -                else []
    1.22 -            val atpset_thms =
    1.23 +        let val atpset_thms =
    1.24                  if include_atpset then ResAxioms.atpset_rules_of ctxt
    1.25                  else []
    1.26              val _ = (Output.debug (fn () => "ATP theorems: ");  app display_thm atpset_thms)
    1.27 -        in  claset_thms @ simpset_thms @ atpset_thms  end
    1.28 +        in  atpset_thms  end
    1.29        val user_rules = filter check_named
    1.30                           (map ResAxioms.pairname
    1.31                             (if null user_thms then whitelist else user_thms))
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Mar 05 20:55:28 2009 +0100
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Mar 05 21:06:59 2009 +0100
     2.3 @@ -15,8 +15,6 @@
     2.4    val expand_defs_tac: thm -> tactic
     2.5    val combinators: thm -> thm
     2.6    val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
     2.7 -  val claset_rules_of: Proof.context -> (string * thm) list   (*FIXME DELETE*)
     2.8 -  val simpset_rules_of: Proof.context -> (string * thm) list  (*FIXME DELETE*)
     2.9    val atpset_rules_of: Proof.context -> (string * thm) list
    2.10    val suppress_endtheory: bool ref     (*for emergency use where endtheory causes problems*)
    2.11    val setup: theory -> theory
    2.12 @@ -378,24 +376,10 @@
    2.13    end;
    2.14  
    2.15  
    2.16 -(**** Extract and Clausify theorems from a theory's claset and simpset ****)
    2.17 +(**** Rules from the context ****)
    2.18  
    2.19  fun pairname th = (Thm.get_name_hint th, th);
    2.20  
    2.21 -fun rules_of_claset cs =
    2.22 -  let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
    2.23 -      val intros = safeIs @ hazIs
    2.24 -      val elims  = map Classical.classical_rule (safeEs @ hazEs)
    2.25 -  in map pairname (intros @ elims) end;
    2.26 -
    2.27 -fun rules_of_simpset ss =
    2.28 -  let val ({rules,...}, _) = rep_ss ss
    2.29 -      val simps = Net.entries rules
    2.30 -  in map (fn r => (#name r, #thm r)) simps end;
    2.31 -
    2.32 -fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt);
    2.33 -fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt);
    2.34 -
    2.35  fun atpset_rules_of ctxt = map pairname (ResAtpset.get ctxt);
    2.36  
    2.37