src/HOL/Tools/ATP/watcher.ML
2006-12-20 paulson 2006-12-20 change from "Array" to "Vector"
2006-10-06 paulson 2006-10-06 Fixed the printing of the used theorems by maintaining separate lists for each subgoal. Retains the ATP input files if debugging is on.
2006-09-28 paulson 2006-09-28 clearout of obsolete code
2006-08-25 paulson 2006-08-25 using inc
2006-04-19 paulson 2006-04-19 fix to spacing in switches, for Vampire under SML/NJ
2006-03-10 paulson 2006-03-10 exporting reapAll and killChild
2006-03-07 mengj 2006-03-07 Proof reconstruction now only takes names of theorems as input.
2006-01-27 paulson 2006-01-27 better reporting
2006-01-14 wenzelm 2006-01-14 Output.debug;
2005-10-10 paulson 2005-10-10 small tidy-up of utility functions
2005-10-07 paulson 2005-10-07 code restructuring
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 moved concat_with_and to watcher.ML
2005-09-28 paulson 2005-09-28 time limit option; fixed bug concerning first line of ATP output
2005-09-22 paulson 2005-09-22 removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
2005-09-21 paulson 2005-09-21 trying to limit the looping
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-09 paulson 2005-09-09 Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
2005-09-08 paulson 2005-09-08 consolidation of duplicate code in Isabelle-ATP linkup
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-09-01 paulson 2005-09-01 improved formatting
2005-08-26 quigley 2005-08-26 DFG output now works for untyped rules (ML "ResClause.untyped();")
2005-08-18 paulson 2005-08-18 no need for TPTP2X unless SPASS is used
2005-07-13 wenzelm 2005-07-13 open ReconPrelim Recon_Transfer;
2005-07-11 quigley 2005-07-11 Fixed some problems with the signal handler.
2005-07-04 quigley 2005-07-04 Streamlined the signal handler in watcher.ML
2005-06-24 paulson 2005-06-24 tidying
2005-06-22 quigley 2005-06-22 Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers. Will now signal if ATP has run out of time and then kill the watcher.
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 vs. File.shell_path;
2005-06-02 quigley 2005-06-02 Added time lime (60 secs) to Spass calls.
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-27 paulson 2005-05-27 Now uses File.write and File.append
2005-05-26 paulson 2005-05-26 further tweaks to the SPASS setup
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-21 paulson 2005-04-21 added hearder lines and deleted some redundant material
2005-04-21 paulson 2005-04-21 improved SML/NJ compatibility, etc.
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-13 paulson 2005-04-13 new signalling primmitives for sml/nj compatibility
2005-04-08 paulson 2005-04-08 Reconstruction code, now packaged to avoid name clashes