| Mon, 29 Mar 2010 18:44:24 +0200 |
blanchet |
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 12:21:51 +0200 |
blanchet |
made "theory_const" a Sledgehammer option;
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 12:01:00 +0200 |
blanchet |
added "respect_no_atp" and "convergence" options to Sledgehammer;
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 14:49:32 +0100 |
blanchet |
added support for Sledgehammer parameters;
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 15:33:18 +0100 |
blanchet |
move all ATP setup code into ATP_Wrapper
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 15:07:44 +0100 |
blanchet |
move the Sledgehammer Isar commands together into one file;
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 13:02:18 +0100 |
blanchet |
more Sledgehammer refactoring
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 19:26:05 +0100 |
blanchet |
renamed Sledgehammer structures
|
file |
diff |
annotate
|
| Fri, 05 Mar 2010 23:51:32 +0100 |
wenzelm |
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2010 22:46:07 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 23:18:03 +0100 |
wenzelm |
Toplevel.thread provides Isar-style exception output;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:59:12 +0100 |
wenzelm |
modernized some structure names;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:09:16 +0100 |
wenzelm |
unregister: eliminated unused status;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 22:18:00 +0100 |
wenzelm |
renamed raw Proof.get_goal to Proof.raw_goal;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 11:25:56 +0100 |
wenzelm |
SimpleThread.fork: uniform handling of outermost Interrupt, which is not an error and should not produce exception trace;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2009 22:16:37 +0200 |
wenzelm |
removed disjunctive group cancellation -- provers run independently;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2009 21:13:29 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 16 Oct 2009 00:26:19 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 17:49:30 +0200 |
wenzelm |
natural argument order for prover;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 17:06:19 +0200 |
wenzelm |
ATP_Manager.get_prover: canonical argument order;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 11:49:27 +0200 |
wenzelm |
eliminated extraneous wrapping of public records;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 11:12:09 +0200 |
wenzelm |
renamed functor HeapFun to Heap;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 10:59:10 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 00:55:29 +0200 |
wenzelm |
structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Wed, 14 Oct 2009 23:44:37 +0200 |
wenzelm |
modernized structure names;
|
file |
diff |
annotate
|
| Sat, 03 Oct 2009 12:10:16 +0200 |
boehmes |
merged
|
file |
diff |
annotate
|
| Sat, 03 Oct 2009 12:05:40 +0200 |
boehmes |
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
|
file |
diff |
annotate
|
| Fri, 02 Oct 2009 23:15:36 +0200 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 16:46:48 +0200 |
nipkow |
made spass additional default prover
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Thu, 03 Sep 2009 17:55:31 +0200 |
boehmes |
added runtime information to sledgehammer
|
file |
diff |
annotate
|
| Sat, 29 Aug 2009 21:57:06 +0200 |
boehmes |
propagate theorem names, in addition to generated return message
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 19:20:24 +0200 |
wenzelm |
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
|
file |
diff |
annotate
| base
|