src/HOL/Tools/ATP/res_clasimpset.ML
2006-04-27 paulson 2006-04-27 slight shortening of blacklist
2006-04-07 mengj 2006-04-07 hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
2006-03-23 mengj 2006-03-23 Only display atpset theorems if Output.show_debug_msgs is true.
2006-03-22 paulson 2006-03-22 Introduction of "whitelist": theorems forced past the relevance filter
2006-03-07 paulson 2006-03-07 Indentation
2006-03-07 mengj 2006-03-07 Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset. The hash table (for removing duplicate) now stores clauses as Term.term with names.
2006-02-28 paulson 2006-02-28 removal of theory blacklist
2006-02-11 mengj 2006-02-11 Changed some code due to changes in reduce_axiomsN.ML.
2006-02-09 paulson 2006-02-09 blacklist tweaks
2006-01-31 paulson 2006-01-31 removal of ResClause.num_of_clauses and other simplifications
2006-01-27 paulson 2006-01-27 tidying
2006-01-27 mengj 2006-01-27 Changed codes that call relevance filter.
2006-01-23 paulson 2006-01-23 ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
2006-01-13 paulson 2006-01-13 blacklist experiments
2005-12-23 paulson 2005-12-23 blacklist of prolific theorems (must be replaced by an attribute later
2005-12-21 paulson 2005-12-21 new hash table module in HOL/Too/s
2005-12-16 paulson 2005-12-16 hashing to eliminate the output of duplicate clauses
2005-11-10 paulson 2005-11-10 duplicate axioms in ATP linkup, and general fixes
2005-10-11 paulson 2005-10-11 simplifying the treatment of nameless theorems
2005-10-05 paulson 2005-10-05 improved process handling. tidied
2005-09-23 paulson 2005-09-23 changed defaults
2005-09-20 paulson 2005-09-20 tidying, and support for axclass/classrel clauses
2005-09-19 paulson 2005-09-19 simplification of the Isabelle-ATP code; hooks for batch generation of problems
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-07 paulson 2005-09-07 axioms now included in tptp files, no /bin/cat and various tidying
2005-09-05 wenzelm 2005-09-05 curried_lookup/update;
2005-09-02 paulson 2005-09-02 further tidying up of Isabelle-ATP link
2005-08-26 quigley 2005-08-26 DFG output now works for untyped rules (ML "ResClause.untyped();")
2005-07-29 paulson 2005-07-29 nameless theorems: better names, flag to omit them
2005-07-28 paulson 2005-07-28 invents theorem names; also patches write_out_clasimp
2005-07-28 quigley 2005-07-28 Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
2005-07-22 paulson 2005-07-22 dead code removal
2005-07-20 paulson 2005-07-20 code streamlining
2005-07-13 paulson 2005-07-13 relevance filtering is now optional
2005-07-07 paulson 2005-07-07 inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
2005-06-10 quigley 2005-06-10 All subgoals sent to the watcher at once now. Rules added to parser for Spass proofs. If parsing or translation fails on a proof, the Spass proof is printed out in PG.
2005-06-01 paulson 2005-06-01 small tweaks; also now write_out_clasimp takes the current theory as argument
2005-05-31 quigley 2005-05-31 Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass ruleset.
2005-05-24 paulson 2005-05-24 A new structure and reduced indentation
2005-05-23 quigley 2005-05-23 Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML. Changed watcher.ML so that the Unix.execute and Unix.reap functions are used instead of those in modUnix.ML, and consequently removed modUnix.ML from Reconstruction.thy
2005-05-12 paulson 2005-05-12 theorem names for caching
2005-05-03 quigley 2005-05-03 Replaced reference to SPASS with general one - set SPASS_HOME in settings file. Rewrote res_clasimpset.ML. Now produces an array of (thm, clause) in addition to writing out clasimpset as tptp strings. C.Q.
2005-05-02 paulson 2005-05-02 deleted redundant code
2005-04-28 paulson 2005-04-28 fixed treatment of higher-order simprules
2005-04-21 paulson 2005-04-21 added hearder lines and deleted some redundant material
2005-04-20 quigley 2005-04-20 Corrected the problem with the ATP directory.
2005-04-19 paulson 2005-04-19 more tidying of libraries in Reconstruction
2005-04-15 paulson 2005-04-15 more tidying up of the SPASS interface
2005-04-12 paulson 2005-04-12 tweaks mainly to achieve sml/nj compatibility
2005-03-31 quigley 2005-03-31 *** empty log message ***