src/HOL/Tools/ATP/watcher.ML
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
2005-04-07 quigley 2005-04-07 Changed prob1.dfg to prob_1.dfg
2005-04-06 quigley 2005-04-06 watcher.ML and watcher.sig changed. Debug files now write to tmp.
2005-04-04 quigley 2005-04-04 CVSfj  ------------------------------------------------------------------- --------------------------------------------------------------- Temporarily added until res_axioms.ML is altered.
2005-03-31 quigley 2005-03-31 *** empty log message ***