# HG changeset patch # User paulson # Date 1127463967 -7200 # Node ID cd555d5a32543b7a72b676643a9118ce3b640277 # Parent 3e3a30bf702f9e5a6ac216c5ea75eabe60f18a79 changed defaults diff -r 3e3a30bf702f -r cd555d5a3254 src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Fri Sep 23 10:25:55 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Fri Sep 23 10:26:07 2005 +0200 @@ -22,10 +22,8 @@ fun term_consts_rm ncs t = add_term_consts_rm ncs t []; - fun thm_consts_rm ncs thm = term_consts_rm ncs (prop_of thm); - fun consts_of_thm (n,thm) = thm_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] thm; fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term; @@ -33,8 +31,6 @@ fun make_pairs [] _ = [] | make_pairs (x::xs) y = (x,y)::(make_pairs xs y); - - fun const_thm_list_aux [] cthms = cthms | const_thm_list_aux (thm::thms) cthms = let val consts = consts_of_thm thm @@ -80,12 +76,10 @@ in relevant_axioms_aux1 consts 1 end; - fun relevant_filter n goal thms = if n<=0 then thms else #2 (relevant_axioms goal (make_thm_table thms) n); - (* find the thms from thy that contain relevant constants, n is the iteration number *) fun find_axioms_n thy goal n = let val clasetR = ResAxioms.claset_rules_of_thy thy @@ -95,7 +89,6 @@ relevant_axioms goal table n end; - fun find_axioms_n_c thy goal n = let val current_thms = PureThy.thms_of thy val table = make_thm_table current_thms @@ -119,7 +112,7 @@ structure ResClasimp : RES_CLASIMP = struct val use_simpset = ref false; (*Performance is much better without simprules*) -val use_nameless = ref false; (*Because most are useless [iff] rules*) +val use_nameless = ref true; val relevant = ref 0; (*Relevance filtering is off by default*) @@ -136,9 +129,6 @@ else ("HOL.TrueI",TrueI) | put_name_pair (a,th) = (a,th); -(* changed, now it also finds out the name of the theorem. *) -(* convert a theorem into CNF and then into Clause.clause format. *) - (* outputs a list of (thm,clause) pairs *) fun multi x 0 xlist = xlist