| Mon, 23 Sep 2013 14:53:43 +0200 |
blanchet |
added "spy" option to Sledgehammer
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
merged "isar_try0" and "isar_minimize" options
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
hardcoded obscure option
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
hard-coded an obscure option
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
use configuration mechanism for low-level tracing
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
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 |
blanchet |
tuning (use a blacklist instead of a whitelist)
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 23:03:21 +0200 |
blanchet |
fixed subtle bug with "take" + thread overlord through
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 16:03:13 +0200 |
blanchet |
have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 22:45:48 +0200 |
wenzelm |
prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 22:15:45 +0200 |
wenzelm |
some protocol to determine provers according to ML;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 19:54:16 +0200 |
wenzelm |
always enable "minimize" to simplify interaction model;
|
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 12:21:25 +0200 |
wenzelm |
eliminated pointless subgoal argument;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2013 12:13:53 +0200 |
wenzelm |
more direct sledgehammer configuration via mode = Normal_Result and output_result;
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 17:57:51 +0200 |
wenzelm |
clarified Query_Operation.register: avoid hard-wired parallel policy;
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 14:24:21 +0200 |
wenzelm |
dockable window for Sledgehammer, based on asynchronous/parallel query operation;
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 21:02:41 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 00:50:49 +0200 |
wenzelm |
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 23:45:05 +0200 |
wenzelm |
system options for Isabelle/HOL proof tools;
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 22:41:25 +0200 |
smolkas |
added sledgehammer parameters isar_try0 and isar_minimize and their negative aliases
|
file |
diff |
annotate
|
| Tue, 09 Jul 2013 18:45:06 +0200 |
smolkas |
completely rewrote SH compress; added two parameters for experimentation/fine grained control
|
file |
diff |
annotate
|
| Tue, 11 Jun 2013 16:13:19 -0400 |
smolkas |
make use of show_type_emphasis instead of using hack; make sure global configurations don't affect proof script creation
|
file |
diff |
annotate
|
| Tue, 21 May 2013 09:02:58 +0200 |
blanchet |
added compatibility alias
|
file |
diff |
annotate
|
| Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 15 May 2013 23:00:17 +0200 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Wed, 15 May 2013 22:30:24 +0200 |
wenzelm |
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
|
file |
diff |
annotate
|
| Wed, 15 May 2013 20:22:46 +0200 |
wenzelm |
maintain ProofGeneral preferences within ProofGeneral module;
|
file |
diff |
annotate
|
| Wed, 15 May 2013 17:39:41 +0200 |
wenzelm |
just one ProofGeneral module;
|
file |
diff |
annotate
|
| Wed, 15 May 2013 17:43:42 +0200 |
blanchet |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file |
diff |
annotate
|