| Mon, 16 Dec 2013 12:02:28 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 09:48:26 +0100 |
blanchet |
added 'meson' to the mix
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 08:35:03 +0100 |
blanchet |
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 18:01:38 +0100 |
blanchet |
robustness in degenerate case + tuning
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 06:33:46 +0100 |
blanchet |
adapted code for Z3 proof reconstruction
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 18:38:25 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 23:03:22 +0200 |
blanchet |
fixed pattern matching
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 19:13:28 +0200 |
wenzelm |
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 11:34:50 +0200 |
wenzelm |
more explicit sendback propertries based on mode;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 09:58:08 +0200 |
blanchet |
whitepsace tuning
|
file |
diff |
annotate
|
| Thu, 18 Jul 2013 20:53:22 +0200 |
wenzelm |
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 21:07:34 +0200 |
smolkas |
added blast, force
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 20:08:06 +0200 |
smolkas |
optimize isar-proofs by trying different proof methods
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 13:33:19 +0200 |
smolkas |
tuned
|
file |
diff |
annotate
|
| Tue, 09 Jul 2013 18:44:59 +0200 |
smolkas |
moved code -> easier debugging
|
file |
diff |
annotate
|