doc-src/Sledgehammer/sledgehammer.tex
2012-04-22 blanchet 2012-04-22 fixed typos
2012-04-21 blanchet 2012-04-21 swap out Satallax, pull in E-SInE again -- it's not clear yet how useful Satallax is after proof reconstruction, whereas E-SInE performed surprisingly well on latest evaluations
2012-04-19 blanchet 2012-04-19 doc update
2012-04-18 blanchet 2012-04-18 update documentation (mostly based on feedback by Makarius)
2012-04-18 blanchet 2012-04-18 doc update
2012-03-21 blanchet 2012-03-21 doc update
2012-03-20 blanchet 2012-03-20 doc update
2012-03-20 blanchet 2012-03-20 document "dont_preplay"
2012-02-24 blanchet 2012-02-24 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
2012-02-24 blanchet 2012-02-24 doc fixes (thanks to Nik)
2012-02-06 blanchet 2012-02-06 renamed type encoding
2012-02-04 blanchet 2012-02-04 fixed docs
2012-02-04 blanchet 2012-02-04 made option available to users (mostly for experiments)
2012-01-30 blanchet 2012-01-30 docs and news
2012-01-19 blanchet 2012-01-19 minor edits in docs
2012-01-19 blanchet 2012-01-19 updated Sledge docs some more
2012-01-19 blanchet 2012-01-19 more doc updates
2012-01-19 blanchet 2012-01-19 updated docs
2012-01-17 blanchet 2012-01-17 improve installation instructions
2011-12-21 blanchet 2011-12-21 updated docs
2011-12-14 blanchet 2011-12-14 updated Sledgehammer/SMT docs
2011-12-01 blanchet 2011-12-01 updated Sledgehammer docs with new/renamed options
2011-11-18 blanchet 2011-11-18 updated Sledgehammer docs
2011-11-16 blanchet 2011-11-16 document metis options better
2011-11-16 blanchet 2011-11-16 document "lam_trans" option
2011-11-06 blanchet 2011-11-06 updated documentation
2011-11-04 blanchet 2011-11-04 document new experimental provers
2011-10-29 blanchet 2011-10-29 specify proof output level 1 (i.e. no detailed, potentially huge E proofs) to LEO-II; requires version 1.2.9
2011-10-17 blanchet 2011-10-17 updated doc related to Satallax
2011-09-23 blanchet 2011-09-23 reintroduced E-SInE now that it's unexpectedly working again (thanks to Geoff)
2011-09-22 blanchet 2011-09-22 take out remote E-SInE -- it's broken and Geoff says it might take quite a while before he gets to it, plus it's fairly obsolete in the meantime
2011-09-07 blanchet 2011-09-07 update Sledgehammer docs
2011-09-07 blanchet 2011-09-07 updated Sledgehammer documentation
2011-09-06 blanchet 2011-09-06 updated Sledgehammer's docs
2011-08-25 blanchet 2011-08-25 rationalized option names -- mono becomes raw_mono and mangled becomes mono
2011-08-23 blanchet 2011-08-23 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
2011-08-23 blanchet 2011-08-23 updated Z3 docs
2011-08-23 blanchet 2011-08-23 update the Vampire related parts of the documentation
2011-08-22 blanchet 2011-08-22 renamed "heavy" to "uniform", based on discussion with Nick Smallbone
2011-08-09 blanchet 2011-08-09 document local HOATPs
2011-08-09 blanchet 2011-08-09 updated Sledgehammer docs
2011-07-26 blanchet 2011-07-26 updated Sledgehammer documentation
2011-07-14 blanchet 2011-07-14 clarify fine soundness point
2011-07-01 blanchet 2011-07-01 update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
2011-07-01 blanchet 2011-07-01 document "simple_higher" type encoding
2011-06-27 blanchet 2011-06-27 document "sound" option
2011-06-27 blanchet 2011-06-27 removed "full_types" option from documentation
2011-06-10 blanchet 2011-06-10 fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day
2011-06-08 blanchet 2011-06-08 removed removed option from documentation
2011-06-07 blanchet 2011-06-07 documentation tweaks
2011-06-07 blanchet 2011-06-07 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
2011-06-06 blanchet 2011-06-06 minor: curly brackets, not square brackets
2011-06-06 blanchet 2011-06-06 document metis better in Sledgehammer docs
2011-06-06 blanchet 2011-06-06 remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"
2011-06-06 blanchet 2011-06-06 don't mention "metisX" so much in the docs -- it will go away soon
2011-06-06 blanchet 2011-06-06 temporarily document "metisX"
2011-05-30 blanchet 2011-05-30 document new explicit apply
2011-05-30 blanchet 2011-05-30 update minimization documentation
2011-05-30 blanchet 2011-05-30 imported patch sledge_doc_metis_as_prover
2011-05-27 blanchet 2011-05-27 new timeout section (cf. Nitpick manual)