| Fri, 16 May 2014 19:13:50 +0200 |
blanchet |
silence methods even better
|
file |
diff |
annotate
|
| Thu, 15 May 2014 20:48:13 +0200 |
blanchet |
new approach to silence proof methods, to avoid weird theory/context mismatches
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:14:58 +0200 |
blanchet |
improved whitelist (cf. be1874de8344)
|
file |
diff |
annotate
|
| Sat, 19 Apr 2014 19:52:02 +0200 |
wenzelm |
more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 14:59:36 +0200 |
wenzelm |
more uniform ML/document antiquotations;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 10:28:08 +0200 |
wenzelm |
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
integrate SMT2 with Sledgehammer
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 10:33:57 +0100 |
blanchet |
restored old 'remotify' logic -- too many bugs were introduced when refactoring the code
|
file |
diff |
annotate
|
| Thu, 13 Feb 2014 16:21:43 +0100 |
blanchet |
do the right thing with provers that exist only remotely (e.g. e_sine)
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 17:13:31 +0100 |
blanchet |
added 'smt' option to control generation of 'by smt' proofs
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 15:33:18 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 10:19:19 +0100 |
blanchet |
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
|
| Fri, 31 Jan 2014 12:30:54 +0100 |
blanchet |
refactor large ML file
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed many Sledgehammer ML files to clarify structure
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
tuned ML file name
|
file |
diff |
annotate
| base
|