src/Doc/Sledgehammer/document/root.tex
17 months ago blanchet 2017-11-07 integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
19 months ago blanchet 2017-09-30 updated Sledgehammer docs
20 months ago blanchet 2017-08-07 use TFF0 with E 2.0 and above
2017-04-20 blanchet 2017-04-20 removed French accent from docs
2016-08-30 blanchet 2016-08-30 tuned docs
2016-03-28 blanchet 2016-03-28 updated Sledgehammer documentation
2015-10-02 blanchet 2015-10-02 updated docs and NEWS
2015-10-02 blanchet 2015-10-02 removed obsolete material in documentation
2015-09-30 blanchet 2015-09-30 updated docs
2015-08-28 blanchet 2015-08-28 eliminated obsolete environment variable
2015-06-25 blanchet 2015-06-25 put E before (typically remote, hence less reliable) Vampire
2015-05-28 blanchet 2015-05-28 made Auto Sledgehammer behave more like the real thing
2015-05-23 wenzelm 2015-05-23 prefer lmodern, which produces scalable T1 fonts even with Debian-ized TeXLive;
2015-04-08 blanchet 2015-04-08 updated docs to reflect actually run ATPs
2015-04-08 blanchet 2015-04-08 updated docs to Z3 open source
2015-03-03 blanchet 2015-03-03 SPASS-Pirate is now called Pirate
2015-02-11 blanchet 2015-02-11 updated Sledgehammer docs
2014-11-24 blanchet 2014-11-24 renamed 'veriT' to 'verit', to stick to all-lowercase rule for prover names
2014-11-24 blanchet 2014-11-24 update CVC4 version docs
2014-09-30 blanchet 2014-09-30 updated docs with two provers: veriT and Zipperposition
2014-08-28 blanchet 2014-08-28 clarified docs
2014-08-04 blanchet 2014-08-04 updated 'compress' docs
2014-08-01 blanchet 2014-08-01 update documentation after removal of 'min' subcommand
2014-08-01 blanchet 2014-08-01 removed proof methods as provers from docs
2014-07-30 blanchet 2014-07-30 updated docs
2014-07-30 blanchet 2014-07-30 reduced preplay timeout to 1 s
2014-07-24 blanchet 2014-07-24 reenabled MaSh for Isabelle2014 release (hopefully)
2014-07-24 blanchet 2014-07-24 stick to external proofs when invoking E, because they are more detailed and do not merge steps
2014-07-16 blanchet 2014-07-16 disabled MaSh for the Isabelle2014 release, due to a couple of issues
2014-07-09 blanchet 2014-07-09 improved docs
2014-07-09 blanchet 2014-07-09 tuned terminology
2014-07-01 blanchet 2014-07-01 updated docs
2014-06-29 blanchet 2014-06-29 killed Python version of MaSh, now that the SML version works adequately
2014-06-18 blanchet 2014-06-18 enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
2014-06-12 blanchet 2014-06-12 renamed Sledgehammer options
2014-06-12 blanchet 2014-06-12 updated docs
2014-06-12 blanchet 2014-06-12 took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
2014-06-11 blanchet 2014-06-11 updated docs w.r.t. Z3
2014-05-28 blanchet 2014-05-28 changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)
2014-05-27 blanchet 2014-05-27 updated naive Bayes
2014-05-26 blanchet 2014-05-26 renamed 'MaSh' option
2014-05-22 blanchet 2014-05-22 shorten Sledgehammer output, as suggested by Andrei Popescu
2014-05-21 blanchet 2014-05-21 docs
2014-05-20 blanchet 2014-05-20 added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
2014-05-20 blanchet 2014-05-20 added Isabelle system option 'mash'
2014-05-20 blanchet 2014-05-20 updated docs
2014-04-25 blanchet 2014-04-25 updated Z3 version number
2014-04-03 blanchet 2014-04-03 don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
2014-04-03 blanchet 2014-04-03 use Alt-Ergo 0.95.2, the latest and greatest version
2014-04-03 blanchet 2014-04-03 updated Z3 TPTP to 4.3.1+
2014-04-03 blanchet 2014-04-03 updated Why3 version in docs
2014-03-14 blanchet 2014-03-14 updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
2014-03-14 blanchet 2014-03-14 updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
2014-02-05 blanchet 2014-02-05 agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
2014-02-03 blanchet 2014-02-03 renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
2014-02-03 blanchet 2014-02-03 searchable underscores
2014-02-03 blanchet 2014-02-03 added new option to documentation
2014-02-03 blanchet 2014-02-03 reduced preplaying timeout, since (1) Isar proofs are getting better and better as alternatives; (2) the same timeout is used for each step in an Isar proof, where a lower timeout makes more sense
2014-01-30 blanchet 2014-01-30 renamed Sledgehammer options for symmetry between positive and negative versions
2014-01-20 blanchet 2014-01-20 killed obsolete provers from documentation