| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
killed final stops in Sledgehammer and friends
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
early warning when Sledgehammer finds a proof
|
file |
diff |
annotate
|
| Fri, 02 Oct 2015 21:06:32 +0200 |
blanchet |
removed legacy asynchronous mode in Sledgehammer
|
file |
diff |
annotate
|
| Thu, 29 Jan 2015 16:35:29 +0100 |
wenzelm |
more explicit indication of Async_Manager_Legacy as Proof General legacy;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:36:41 +0100 |
wenzelm |
discontinued obsolete Output.urgent_message;
|
file |
diff |
annotate
|
| Sun, 12 Oct 2014 21:52:45 +0200 |
blanchet |
special treatment of extensionality in minimizer
|
file |
diff |
annotate
|
| Tue, 30 Sep 2014 14:54:14 +0200 |
blanchet |
tuned output in case of one-liner failure
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 23:57:26 +0200 |
blanchet |
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
merged minimize and auto_minimize
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
renamed new SMT module from 'SMT2' to 'SMT'
|
file |
diff |
annotate
|
| Mon, 04 Aug 2014 15:02:02 +0200 |
blanchet |
cleaner 'compress' option
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
restored a bit of laziness
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
honor 'try0' also for one-liners
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
eliminated needlessly complex message tail
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
rationalized preplaying by eliminating (now superfluous) laziness
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
simplified minimization logic
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
put faster proof methods first
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
use parallel preplay machinery also for one-line proofs
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
always minimize Sledgehammer results by default
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
added more proof methods for one-liners
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:13 +0200 |
fleury |
Whitespace and indentation correction.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
Basic support for the SMT prover veriT.
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:10:12 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
| Wed, 11 Jun 2014 11:28:46 +0200 |
blanchet |
removed old SMT module from Sledgehammer
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 15:10:18 +0200 |
fleury |
basic setup for zipperposition prover
|
file |
diff |
annotate
|
| Thu, 22 May 2014 05:23:50 +0200 |
blanchet |
properly reconstruct helpers in Z3 proofs
|
file |
diff |
annotate
|
| Thu, 22 May 2014 03:29:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|