2005-10-10 ago small tidy-up of utility functions
2005-10-07 ago minor code tidyig
2005-10-07 ago more tidying. Fixed process management bugs and race condition
2005-10-06 ago major simplification: removal of the goalstring argument
2005-10-05 ago improved process handling. tidied
2005-10-04 ago fixed the ascii-armouring of goalstring
2005-09-29 ago improvements for problem generation
2005-09-28 ago time limit option; fixed bug concerning first line of ATP output
2005-09-20 ago tidying, and support for axclass/classrel clauses
2005-09-20 ago further tidying; killing of old Watcher loops
2005-09-19 ago further simplification of the Isabelle-ATP linkup
2005-09-19 ago simplification of the Isabelle-ATP code; hooks for batch generation of problems
2005-09-16 ago PARTIAL conversion to Vampire8
2005-09-15 ago massive tidy-up and simplification
2005-09-15 ago the experimental tagging system, and the usual tidying
2005-09-09 ago Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
2005-09-07 ago Progress on eprover linkup, also massive tidying
2005-09-07 ago axioms now included in tptp files, no /bin/cat and various tidying
2005-09-02 ago Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
2005-09-02 ago further tidying up of Isabelle-ATP link
2005-09-02 ago tidying up the Isabelle/ATP interface
2005-08-26 ago DFG output now works for untyped rules (ML "ResClause.untyped();")
2005-08-17 ago new command to invoke ATPs
2005-07-28 ago dead code
2005-07-27 ago simpler variable names, and no types for monomorphic constants
2005-07-22 ago tidied up the tracing output
2005-07-20 ago code streamlining
2005-07-13 ago use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
2005-07-11 ago Fixed some problems with the signal handler.
2005-07-07 ago inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
2005-07-04 ago Streamlined the signal handler in watcher.ML
2005-06-21 ago Integrated vampire lemma code.
2005-06-21 ago VAMPIRE_HOME, helper_path and various stylistic tweaks
2005-06-20 ago Added VampCommunication.ML.
2005-06-20 ago using TPTP2X_HOME; indentation, etc
2005-06-10 ago All subgoals sent to the watcher at once now.
2005-06-05 ago File.platform_path;
2005-06-02 ago Added time lime (60 secs) to Spass calls.
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-26 ago trying to set up portable calling sequences for SPASS and tptp2X
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-03 ago Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
2005-04-20 ago Corrected the problem with the ATP directory.
2005-04-20 ago Removed remaining references to Main.thy in reconstruction code.
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-04-11 ago removal of Main and other tidying up
2005-04-07 ago removed bad code
2005-04-07 ago Integrating the reconstruction files into the building of HOL
2005-04-05 ago Current version of res_atp.ML - causes an error when I run it. C.Q.
2005-04-04 ago Updated to add watcher code.
2005-03-31 ago *** empty log message ***
2005-03-14 ago bug fixes involving typechecking clauses
2005-03-11 ago code reformatted
2005-03-04 ago removed dead code
2005-01-21 ago Jia Meng: delta simpsets and clasets
2004-11-30 ago resolution package tools by Jia Meng