--- 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