| Thu, 24 Jul 2014 00:24:00 +0200 |
stick to external proofs when invoking E, because they are more detailed and do not merge steps
|
file | diff | annotate |
| Wed, 16 Jul 2014 17:57:27 +0200 |
disabled MaSh for the Isabelle2014 release, due to a couple of issues
|
file | diff | annotate |
| Wed, 09 Jul 2014 18:48:37 +0200 |
improved docs
|
file | diff | annotate |
| Wed, 09 Jul 2014 11:35:52 +0200 |
tuned terminology
|
file | diff | annotate |
| Tue, 01 Jul 2014 16:47:10 +0200 |
updated docs
|
file | diff | annotate |
| Sun, 29 Jun 2014 18:28:27 +0200 |
killed Python version of MaSh, now that the SML version works adequately
|
file | diff | annotate |
| Wed, 18 Jun 2014 13:23:09 +0200 |
enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
|
file | diff | annotate |
| Thu, 12 Jun 2014 17:10:12 +0200 |
renamed Sledgehammer options
|
file | diff | annotate |
| Thu, 12 Jun 2014 17:02:03 +0200 |
updated docs
|
file | diff | annotate |
| Thu, 12 Jun 2014 17:02:03 +0200 |
took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
|
file | diff | annotate |
| Wed, 11 Jun 2014 11:28:46 +0200 |
updated docs w.r.t. Z3
|
file | diff | annotate |
| Wed, 28 May 2014 17:42:34 +0200 |
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)
|
file | diff | annotate |
| Tue, 27 May 2014 17:48:11 +0200 |
updated naive Bayes
|
file | diff | annotate |
| Mon, 26 May 2014 14:15:48 +0200 |
renamed 'MaSh' option
|
file | diff | annotate |
| Thu, 22 May 2014 03:29:35 +0200 |
shorten Sledgehammer output, as suggested by Andrei Popescu
|
file | diff | annotate |
| Wed, 21 May 2014 14:09:43 +0200 |
docs
|
file | diff | annotate |
| Tue, 20 May 2014 22:28:44 +0200 |
added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
|
file | diff | annotate |
| Tue, 20 May 2014 22:28:08 +0200 |
added Isabelle system option 'mash'
|
file | diff | annotate |
| Tue, 20 May 2014 16:39:13 +0200 |
updated docs
|
file | diff | annotate |
| Fri, 25 Apr 2014 22:13:17 +0200 |
updated Z3 version number
|
file | diff | annotate |
| Thu, 03 Apr 2014 17:16:02 +0200 |
don't pass Vampire option that doesn't exist anymore (and that wasn't strictly necessary with older Vampires)
|
file | diff | annotate |
| Thu, 03 Apr 2014 17:00:14 +0200 |
use Alt-Ergo 0.95.2, the latest and greatest version
|
file | diff | annotate |
| Thu, 03 Apr 2014 16:57:19 +0200 |
updated Z3 TPTP to 4.3.1+
|
file | diff | annotate |
| Thu, 03 Apr 2014 13:29:58 +0200 |
updated Why3 version in docs
|
file | diff | annotate |
| Fri, 14 Mar 2014 01:28:15 +0100 |
updated Sledgehammer docs w.r.t. 'smt2' and 'z3_new'
|
file | diff | annotate |
| Fri, 14 Mar 2014 01:28:14 +0100 |
updated documentation w.r.t. 'z3_non_commercial' option in Isabelle/jEdit
|
file | diff | annotate |
| Wed, 05 Feb 2014 11:47:56 +0100 |
agsyHOL is also called AgsyHOL by Lindblad himself, so let's follow this convention
|
file | diff | annotate |
| Mon, 03 Feb 2014 19:32:02 +0100 |
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
|
file | diff | annotate |
| Mon, 03 Feb 2014 17:55:50 +0100 |
searchable underscores
|
file | diff | annotate |
| Mon, 03 Feb 2014 17:18:38 +0100 |
added new option to documentation
|
file | diff | annotate |
| Mon, 03 Feb 2014 10:19:19 +0100 |
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
|
file | diff | annotate |
| Thu, 30 Jan 2014 14:37:53 +0100 |
renamed Sledgehammer options for symmetry between positive and negative versions
|
file | diff | annotate |
| Mon, 20 Jan 2014 10:07:07 +0100 |
killed obsolete provers from documentation
|
file | diff | annotate |
| Thu, 19 Dec 2013 13:43:21 +0100 |
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
|
file | diff | annotate |
| Tue, 17 Dec 2013 14:03:29 +0100 |
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
|
file | diff | annotate |
| Mon, 09 Dec 2013 04:03:30 +0100 |
added warning to documentation, based on isabelle-users thread
|
file | diff | annotate |
| Thu, 17 Oct 2013 20:03:37 +0200 |
added thread-safety warnings
|
file | diff | annotate |
| Tue, 15 Oct 2013 15:31:32 +0200 |
updated S/H docs
|
file | diff | annotate |
| Tue, 01 Oct 2013 19:58:31 +0200 |
tiny doc fix
|
file | diff | annotate |
| Mon, 23 Sep 2013 14:53:43 +0200 |
document "spy" option
|
file | diff | annotate |
| Sat, 21 Sep 2013 22:48:52 +0200 |
repaired latex (cf. 7bb0cf27c243);
|
file | diff | annotate |
| Fri, 20 Sep 2013 22:39:30 +0200 |
document option
|
file | diff | annotate |
| Fri, 20 Sep 2013 22:39:30 +0200 |
moved focus to Isabell/jEdit and away from Proof General
|
file | diff | annotate |
| Fri, 20 Sep 2013 22:39:30 +0200 |
took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
|
file | diff | annotate |
| Fri, 20 Sep 2013 22:39:30 +0200 |
reduce the number of emitted MaSh commands (among others to facilitate debugging)
|
file | diff | annotate |
| Wed, 11 Sep 2013 10:57:09 +0200 |
updated docs
|
file | diff | annotate |
| Wed, 28 Aug 2013 18:44:50 +0200 |
tuned messages
|
file | diff | annotate |
| Tue, 20 Aug 2013 14:39:55 +0200 |
doc tuning
|
file | diff | annotate |
| Tue, 20 Aug 2013 04:59:25 +0200 |
removed french option to manuals
|
file | diff | annotate |
| Tue, 13 Aug 2013 10:29:49 +0200 |
updated Vampire version numbers
|
file | diff | annotate |
| Mon, 29 Jul 2013 17:27:56 +0200 |
updated Sledgehammer prover versions
|
file | diff | annotate |
| Mon, 20 May 2013 16:12:33 +0200 |
updated Sledgehammer docs
|
file | diff | annotate |
| Wed, 20 Feb 2013 15:26:19 +0100 |
upgraded to Alt-Ergo 0.95
|
file | diff | annotate |
| Wed, 20 Feb 2013 08:44:24 +0100 |
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
|
file | diff | annotate |
| Wed, 20 Feb 2013 08:44:24 +0100 |
alias for people like me
|
file | diff | annotate |
| Thu, 14 Feb 2013 22:49:22 +0100 |
renamed sledgehammer_shrink to sledgehammer_compress
|
file | diff | annotate |
| Thu, 07 Feb 2013 14:05:32 +0100 |
distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
|
file | diff | annotate |
| Thu, 17 Jan 2013 14:06:14 +0100 |
updated docs
|
file | diff | annotate |
| Fri, 04 Jan 2013 19:00:49 +0100 |
updated docs
|
file | diff | annotate |
| Wed, 12 Dec 2012 00:24:06 +0100 |
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
|
file | diff | annotate |