src/HOL/ATP_Linkup.thy
2009-11-10 haftmann 2009-11-10 tuned imports
2009-10-29 wenzelm 2009-10-29 modernized some structure names;
2009-10-14 wenzelm 2009-10-14 modernized structure names;
2009-10-03 boehmes 2009-10-03 re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values, eliminated unused provers, turned references into configuration values
2009-08-04 wenzelm 2009-08-04 src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
2009-06-28 immler 2009-06-28 check for current versions on server
2009-06-28 immler 2009-06-28 relevance filter with the same parameters for remote-versions
2009-06-28 immler 2009-06-28 use X2TPTP optionally and only for remote_spass; append original response if proof is extracted
2009-05-04 immler 2009-05-04 added Philipp Meyer's implementation of AtpMinimal together with related changes in the sledgehammer-interface: adapted type of prover, optional relevance filtering, public get_prover for registered atps in AtpManager, included atp_minimize in s/h response;
2009-01-28 haftmann 2009-01-28 Plain, Main form meeting points in import hierarchy
2009-01-21 haftmann 2009-01-21 merged
2009-01-21 haftmann 2009-01-21 changed import hierarchy
2009-01-21 wenzelm 2009-01-21 merged
2009-01-20 immler 2009-01-20 pass timeout to prover; especially to remote-script
2009-01-20 immler 2009-01-20 modified remote script; modified handling of errors
2009-01-14 immler 2009-01-14 removed useless
2009-01-12 immler 2009-01-12 simplified usage of remote-script; added compatible remote-atps
2009-01-21 haftmann 2009-01-21 dropped ID
2008-10-14 wenzelm 2008-10-14 tuned AtpWrapper interfaces;
2008-10-14 wenzelm 2008-10-14 renamed AtpThread to AtpWrapper;
2008-10-14 wenzelm 2008-10-14 tuned comments;
2008-10-13 wenzelm 2008-10-13 ** Update from Fabian ** added remote prover functions;
2008-10-03 wenzelm 2008-10-03 perform atp_setups here;
2008-10-03 wenzelm 2008-10-03 version of sledgehammer using threads instead of processes, misc cleanup; (by Fabian Immler);
2008-10-03 wenzelm 2008-10-03 removed old/unused setup of raw ATP oracles;
2008-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-06-12 wenzelm 2008-06-12 tuned setup;
2008-04-22 haftmann 2008-04-22 dropped theory PreList
2007-12-22 wenzelm 2007-12-22 use random_word.ML earlier;
2007-12-20 wenzelm 2007-12-20 moved Pure/General/random_word.ML to Tools/random_word.ML;
2007-12-19 paulson 2007-12-19 Replaced refs by config params; finer critical section in mets method
2007-12-10 haftmann 2007-12-10 swtiched ATP_Linkup and PreList in theory hierarchy
2007-10-10 paulson 2007-10-10 removed dead code
2007-10-04 paulson 2007-10-04 combinator translation
2007-10-03 wenzelm 2007-10-03 modernized definitions;
2007-09-27 paulson 2007-09-27 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions
2007-08-18 wenzelm 2007-08-18 renamed ResAtpMethods.setup;
2007-08-15 paulson 2007-08-15 combining the relevance filter with res_atp
2007-08-07 haftmann 2007-08-07 changed import order
2007-07-20 haftmann 2007-07-20 simplified HOL bootstrap
2007-06-29 paulson 2007-06-29 bug fixes to proof reconstruction
2007-06-20 wenzelm 2007-06-20 added Metis setup (from Metis.thy);
2007-01-04 paulson 2007-01-04 improvements to proof reconstruction. Some files loaded in a different order
2007-01-03 paulson 2007-01-03 first version of structured proof reconstruction
2006-11-22 haftmann 2006-11-22 removed Extraction dependency
2006-11-08 wenzelm 2006-11-08 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;