src/HOL/Tools/ATP/recon_transfer_proof.ML
2005-10-07 paulson 2005-10-07 minor code tidyig
2005-10-06 paulson 2005-10-06 major simplification: removal of the goalstring argument
2005-10-04 paulson 2005-10-04 fixed the ascii-armouring of goalstring
2005-09-29 paulson 2005-09-29 reduction in tracing files
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 improved proof parsing
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-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-08 paulson 2005-09-08 yet more tidying of Isabelle-ATP link
2005-09-07 paulson 2005-09-07 Progress on eprover linkup, also massive 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-08-18 paulson 2005-08-18 nicer list of axioms used
2005-07-22 paulson 2005-07-22 reformatting and tidying
2005-07-13 wenzelm 2005-07-13 tuned;
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-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-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-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 further tweaks to the SPASS setup
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-22 paulson 2005-04-22 removed last occurrences of OS.Process.sleep
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-15 paulson 2005-04-15 yet more tidying up: removal of some references to Main
2005-04-12 paulson 2005-04-12 tweaks mainly to achieve sml/nj compatibility
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 ***