changed defaults
authorpaulson
Fri Sep 23 10:26:07 2005 +0200 (2005-09-23)
changeset 17596cd555d5a3254
parent 17595 3e3a30bf702f
child 17597 dac8dd2272cd
changed defaults
src/HOL/Tools/ATP/res_clasimpset.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Sep 23 10:25:55 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Sep 23 10:26:07 2005 +0200
     1.3 @@ -22,10 +22,8 @@
     1.4  
     1.5  fun term_consts_rm ncs t = add_term_consts_rm ncs t [];
     1.6  
     1.7 -
     1.8  fun thm_consts_rm ncs thm = term_consts_rm ncs (prop_of thm);
     1.9  
    1.10 -
    1.11  fun consts_of_thm (n,thm) = thm_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] thm;
    1.12  
    1.13  fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term;
    1.14 @@ -33,8 +31,6 @@
    1.15  fun make_pairs [] _ = []
    1.16    | make_pairs (x::xs) y = (x,y)::(make_pairs xs y);
    1.17  
    1.18 -
    1.19 -
    1.20  fun const_thm_list_aux [] cthms = cthms
    1.21    | const_thm_list_aux (thm::thms) cthms =
    1.22      let val consts = consts_of_thm thm
    1.23 @@ -80,12 +76,10 @@
    1.24  
    1.25      in  relevant_axioms_aux1 consts 1  end;
    1.26  
    1.27 -
    1.28  fun relevant_filter n goal thms = 
    1.29      if n<=0 then thms 
    1.30      else #2 (relevant_axioms goal (make_thm_table thms) n);
    1.31  
    1.32 -
    1.33  (* find the thms from thy that contain relevant constants, n is the iteration number *)
    1.34  fun find_axioms_n thy goal n =
    1.35      let val clasetR = ResAxioms.claset_rules_of_thy thy
    1.36 @@ -95,7 +89,6 @@
    1.37  	relevant_axioms goal table n
    1.38      end;
    1.39  
    1.40 -
    1.41  fun find_axioms_n_c thy goal n =
    1.42      let val current_thms = PureThy.thms_of thy
    1.43  	val table = make_thm_table current_thms
    1.44 @@ -119,7 +112,7 @@
    1.45  structure ResClasimp : RES_CLASIMP =
    1.46  struct
    1.47  val use_simpset = ref false;   (*Performance is much better without simprules*)
    1.48 -val use_nameless = ref false;  (*Because most are useless [iff] rules*)
    1.49 +val use_nameless = ref true;
    1.50  
    1.51  val relevant = ref 0;  (*Relevance filtering is off by default*)
    1.52  
    1.53 @@ -136,9 +129,6 @@
    1.54                              else ("HOL.TrueI",TrueI)
    1.55    | put_name_pair (a,th)  = (a,th);
    1.56  
    1.57 -(* changed, now it also finds out the name of the theorem. *)
    1.58 -(* convert a theorem into CNF and then into Clause.clause format. *)
    1.59 -
    1.60  (* outputs a list of (thm,clause) pairs *)
    1.61  
    1.62  fun multi x 0 xlist = xlist