| Wed, 21 Apr 2010 16:21:19 +0200 |
blanchet |
pass relevant options from "sledgehammer" to "sledgehammer minimize";
|
file |
diff |
annotate
|
| Tue, 20 Apr 2010 17:41:00 +0200 |
blanchet |
use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 19:41:15 +0200 |
blanchet |
don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 18:44:12 +0200 |
blanchet |
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 15:21:35 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 15:15:21 +0200 |
blanchet |
make Sledgehammer's minimizer also minimize Isar proofs
|
file |
diff |
annotate
|
| Wed, 14 Apr 2010 21:22:13 +0200 |
blanchet |
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
|
file |
diff |
annotate
|
| Wed, 14 Apr 2010 18:23:51 +0200 |
blanchet |
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
|
file |
diff |
annotate
|
| 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
|
| 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
|
| Fri, 06 Nov 2009 19:22:32 +0100 |
nipkow |
Command atp_minimize uses the naive linear algorithm now
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:59:12 +0100 |
wenzelm |
modernized some structure names;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 14:54:14 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 22:18:00 +0100 |
wenzelm |
renamed raw Proof.get_goal to Proof.raw_goal;
|
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 12:23:24 +0200 |
wenzelm |
misc tuning and recovery of Isabelle coding style;
|
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 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:05:40 +0200 |
boehmes |
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Mon, 14 Sep 2009 19:30:48 +0200 |
nipkow |
count number of iterations required for minimization (and fixed bug: minimization was always called)
|
file |
diff |
annotate
|
| Mon, 07 Sep 2009 22:08:05 +0200 |
nipkow |
Fixed "minimal" to cover the case that "p []" holds (excluded in the article by Bradley & Manna)
|
file |
diff |
annotate
|
| Sat, 05 Sep 2009 22:01:31 +0200 |
boehmes |
added signature ATP_MINIMAL,
|
file |
diff |
annotate
|
| Thu, 03 Sep 2009 17:55:31 +0200 |
boehmes |
added runtime information to sledgehammer
|
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
|