| Wed, 20 Feb 2013 08:44:24 +0100 |
blanchet |
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 |
blanchet |
alias for people like me
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:26 +0100 |
blanchet |
killed legacy alias
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 22:49:22 +0100 |
smolkas |
renamed sledgehammer_shrink to sledgehammer_compress
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 14:35:28 +0100 |
smolkas |
tuned
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 13:57:51 +0100 |
smolkas |
set show_markup to false in order to avoid problems in jedit
|
file |
diff |
annotate
|
| Sat, 05 Jan 2013 22:31:30 +0100 |
blanchet |
nicer output
|
file |
diff |
annotate
|
| Sat, 05 Jan 2013 22:31:30 +0100 |
blanchet |
pass option to minimize
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 19:00:49 +0100 |
blanchet |
renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)
|
file |
diff |
annotate
|
| Wed, 19 Dec 2012 22:43:07 +0100 |
blanchet |
crank up default timeout for MaSh ATP learning
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 19:57:12 +0100 |
blanchet |
thread no timeout properly
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 00:24:06 +0100 |
blanchet |
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
|
file |
diff |
annotate
|
| Mon, 12 Nov 2012 14:11:51 +0100 |
blanchet |
create temp directory if not already created
|
file |
diff |
annotate
|
| Tue, 06 Nov 2012 15:15:33 +0100 |
blanchet |
renamed Sledgehammer option
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 15:05:17 +0200 |
blanchet |
renamed Isar-proof related options + changed semantics of Isar shrinking
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 09:12:50 +0200 |
blanchet |
tuned message
|
file |
diff |
annotate
|
| Fri, 14 Sep 2012 12:09:27 +0200 |
blanchet |
merged two commands
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 11:07:27 +0200 |
blanchet |
detect unknown options again
|
file |
diff |
annotate
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
don't relearn old facts in Isar mode
|
file |
diff |
annotate
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
honor suggested MaSh weights
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
use CVC3 and Yices by default if they are available and there are enough cores
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
minimal maxes + tuning
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learn from SMT proofs when they can be minimized by Metis
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
convenience
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learning should honor the fact override and the chained facts
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
added "learn_from_atp" command to MaSh, for patient users
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
more MaSh docs
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learn command in MaSh
|
file |
diff |
annotate
|