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