src/HOL/Tools/ATP/res_clasimpset.ML
2005-10-05 ago improved process handling. tidied
2005-09-23 ago changed defaults
2005-09-20 ago tidying, and support for axclass/classrel clauses
2005-09-19 ago simplification of the Isabelle-ATP code; hooks for batch generation of problems
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-07 ago axioms now included in tptp files, no /bin/cat and various tidying
2005-09-05 ago curried_lookup/update;
2005-09-02 ago further tidying up of Isabelle-ATP link
2005-08-26 ago DFG output now works for untyped rules (ML "ResClause.untyped();")
2005-07-29 ago nameless theorems: better names, flag to omit them
2005-07-28 ago invents theorem names; also patches write_out_clasimp
2005-07-28 ago Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
2005-07-22 ago dead code removal
2005-07-20 ago code streamlining
2005-07-13 ago relevance filtering is now optional
2005-07-07 ago inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
2005-06-10 ago All subgoals sent to the watcher at once now.
2005-06-01 ago small tweaks; also now write_out_clasimp takes the current theory as argument
2005-05-31 ago Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
2005-05-24 ago A new structure and reduced indentation
2005-05-23 ago Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
2005-05-12 ago theorem names for caching
2005-05-03 ago Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
2005-05-02 ago deleted redundant code
2005-04-28 ago fixed treatment of higher-order simprules
2005-04-21 ago added hearder lines and deleted some redundant material
2005-04-20 ago Corrected the problem with the ATP directory.
2005-04-19 ago more tidying of libraries in Reconstruction
2005-04-15 ago more tidying up of the SPASS interface
2005-04-12 ago tweaks mainly to achieve sml/nj compatibility
2005-03-31 ago *** empty log message ***