src/HOL/Tools/ATP/recon_parse.ML
2005-12-20 haftmann 2005-12-20 removed superfluos is_prefix functions
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-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-07-28 paulson 2005-07-28 uniform treatment of variable prefixes
2005-07-14 wenzelm 2005-07-14 replaced Utils.itlist by fold_rev;
2005-07-13 wenzelm 2005-07-13 open ReconPrelim ReconTranslateProof; removed second copy of exception ASSERTION;
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-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-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 paulson 2005-04-21 added hearder lines and deleted some redundant material
2005-04-09 paulson 2005-04-09 fixed the syntax of infix declarations
2005-04-08 paulson 2005-04-08 Reconstruction code, now packaged to avoid name clashes
2005-03-31 quigley 2005-03-31 *** empty log message ***