src/HOL/Tools/res_atp.ML
2006-01-27 paulson 2006-01-27 tidying up SPASS output
2006-01-23 paulson 2006-01-23 ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
2006-01-17 paulson 2006-01-17 improved SPASS support
2006-01-14 wenzelm 2006-01-14 Output.debug;
2006-01-13 paulson 2006-01-13 more practical time limit
2005-12-14 paulson 2005-12-14 removed unused function repeat_RS
2005-11-28 mengj 2005-11-28 Only output arities and class relations if !ResClause.keep_types is true.
2005-10-28 mengj 2005-10-28 Added "writeln_strs" to the signature
2005-10-18 paulson 2005-10-18 new interface to make_conjecture_clauses
2005-10-14 paulson 2005-10-14 signature changes
2005-10-14 paulson 2005-10-14 deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
2005-10-10 paulson 2005-10-10 small tidy-up of utility functions
2005-10-07 paulson 2005-10-07 minor code tidyig
2005-10-07 paulson 2005-10-07 more tidying. Fixed process management bugs and race condition
2005-10-06 paulson 2005-10-06 major simplification: removal of the goalstring argument
2005-10-05 paulson 2005-10-05 improved process handling. tidied
2005-10-04 paulson 2005-10-04 fixed the ascii-armouring of goalstring
2005-09-29 paulson 2005-09-29 improvements for problem generation
2005-09-28 paulson 2005-09-28 time limit option; fixed bug concerning first line of ATP output
2005-09-20 paulson 2005-09-20 tidying, and support for axclass/classrel clauses
2005-09-20 paulson 2005-09-20 further tidying; killing of old Watcher loops
2005-09-19 paulson 2005-09-19 further simplification of the Isabelle-ATP linkup
2005-09-19 paulson 2005-09-19 simplification of the Isabelle-ATP code; hooks for batch generation of problems
2005-09-16 paulson 2005-09-16 PARTIAL conversion to Vampire8
2005-09-15 paulson 2005-09-15 massive tidy-up and simplification
2005-09-15 paulson 2005-09-15 the experimental tagging system, and the usual tidying
2005-09-09 paulson 2005-09-09 Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
2005-09-07 paulson 2005-09-07 Progress on eprover linkup, also massive tidying
2005-09-07 paulson 2005-09-07 axioms now included in tptp files, no /bin/cat and various tidying
2005-09-02 quigley 2005-09-02 Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and recon_transfer_proof.ML to deal with the E theorem prover.
2005-09-02 paulson 2005-09-02 further tidying up of Isabelle-ATP link
2005-09-02 paulson 2005-09-02 tidying up the Isabelle/ATP interface
2005-08-26 quigley 2005-08-26 DFG output now works for untyped rules (ML "ResClause.untyped();")
2005-08-17 paulson 2005-08-17 new command to invoke ATPs
2005-07-28 paulson 2005-07-28 dead code
2005-07-27 paulson 2005-07-27 simpler variable names, and no types for monomorphic constants
2005-07-22 paulson 2005-07-22 tidied up the tracing output
2005-07-20 paulson 2005-07-20 code streamlining
2005-07-13 wenzelm 2005-07-13 use Toplevel.print_state_hook instead of adhoc Proof.atp_hook; added call_atp: bool ref; do 'setmp print_mode []', which is more robust than manual ref manipulation; added subtract_simpset, subtract_claset (supercede delta approximation);
2005-07-11 quigley 2005-07-11 Fixed some problems with the signal handler.
2005-07-07 paulson 2005-07-07 inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
2005-07-04 quigley 2005-07-04 Streamlined the signal handler in watcher.ML
2005-06-21 quigley 2005-06-21 Integrated vampire lemma code.
2005-06-21 paulson 2005-06-21 VAMPIRE_HOME, helper_path and various stylistic tweaks
2005-06-20 quigley 2005-06-20 Added VampCommunication.ML. Changed small set of Spass rules to Ordered version. Fixed printing out of resolution proofs if parsing/translation fails.
2005-06-20 paulson 2005-06-20 using TPTP2X_HOME; indentation, etc
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-05 wenzelm 2005-06-05 File.platform_path;
2005-06-02 quigley 2005-06-02 Added time lime (60 secs) to Spass calls.
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-26 paulson 2005-05-26 trying to set up portable calling sequences for SPASS and tptp2X
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-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-04-20 quigley 2005-04-20 Corrected the problem with the ATP directory.
2005-04-20 quigley 2005-04-20 Removed remaining references to Main.thy in reconstruction code.
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