doc-src/Sledgehammer/sledgehammer.tex
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)
2011-05-27 blanchet 2011-05-27 more Sledgehammer documentation updates
2011-05-27 blanchet 2011-05-27 minor update
2011-05-27 blanchet 2011-05-27 more concise output
2011-05-27 blanchet 2011-05-27 minor fixes to Sledgehammer docs
2011-05-27 blanchet 2011-05-27 readded Waldmeister as default to the documentation and other minor changes
2011-05-27 blanchet 2011-05-27 renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
2011-05-27 blanchet 2011-05-27 minor doc adjustments
2011-05-27 blanchet 2011-05-27 merge timeout messages from several ATPs into one message to avoid clutter
2011-05-27 blanchet 2011-05-27 mention contributions from LCP and explain metis and metisFT encodings
2011-05-27 blanchet 2011-05-27 document relevance filter a bit more
2011-05-27 blanchet 2011-05-27 always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
2011-05-24 blanchet 2011-05-24 document primitive support for LEO-II and Satallax
2011-05-22 blanchet 2011-05-22 slightly improved documentation
2011-05-22 blanchet 2011-05-22 document Waldmeister
2011-05-20 blanchet 2011-05-20 added see also
2011-05-20 blanchet 2011-05-20 document new type system and soundness properties of the different systems
2011-05-20 blanchet 2011-05-20 more doc fiddling
2011-05-20 blanchet 2011-05-20 more FAQs
2011-05-20 blanchet 2011-05-20 updated FAQ
2011-05-19 blanchet 2011-05-19 updated option documentation
2011-05-19 blanchet 2011-05-19 distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job
2011-05-19 blanchet 2011-05-19 minor doc fixes
2011-05-19 blanchet 2011-05-19 mention version 0.6 of Vampire, since that's what's currently available for download
2011-05-12 blanchet 2011-05-12 added hints and FAQs
2011-05-12 blanchet 2011-05-12 drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
2011-05-12 blanchet 2011-05-12 reflect option renaming in doc + do not document the type systems poly_preds? and poly_tags?, since they are virtually identical to the non-? versions
2011-05-12 blanchet 2011-05-12 ensure that Auto Sledgehammer is run with full type information
2011-05-12 blanchet 2011-05-12 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
2011-05-12 blanchet 2011-05-12 renamed type systems for more consistency
2011-05-04 blanchet 2011-05-04 documentation tuning
2011-05-04 blanchet 2011-05-04 update type system documentation