2005-10-07 wenzelm 2005-10-07 Term.str_of_term;
2005-09-19 paulson 2005-09-19 further simplification of the Isabelle-ATP linkup
2005-09-14 haftmann 2005-09-14 introduces AList.lookup
2005-09-08 paulson 2005-09-08 yet more tidying of Isabelle-ATP link
2005-07-13 wenzelm 2005-07-13 tuned;
2005-07-06 wenzelm 2005-07-06 added adhoc string_of_term from Pure/term.ML;
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-17 wenzelm 2005-06-17 Theory.merge;
2005-06-17 quigley 2005-06-17 Multiple subgoals working.
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-05-31 paulson 2005-05-31 minor tidying and sml/nj compatibility
2005-05-24 paulson 2005-05-24 A new structure and reduced indentation
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 berghofe 2005-04-21 Adapted to new interface of instantiation and unification / matching functions.
2005-04-21 paulson 2005-04-21 added hearder lines and deleted some redundant material
2005-04-19 paulson 2005-04-19 more tidying of libraries in Reconstruction
2005-04-15 paulson 2005-04-15 yet more tidying up: removal of some references to Main
2005-04-15 paulson 2005-04-15 more tidying up of the SPASS interface
2005-04-11 paulson 2005-04-11 removal of Main and other tidying up
2005-04-08 paulson 2005-04-08 Reconstruction code, now packaged to avoid name clashes
2005-04-06 quigley 2005-04-06 watcher.ML and watcher.sig changed. Debug files now write to tmp.
2005-03-31 quigley 2005-03-31 *** empty log message ***