src/HOL/Tools/ATP/res_clasimpset.ML
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 ***