| 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
|
| Sun, 04 Oct 2009 11:45:41 +0200 |
boehmes |
avoid exception Option: only apply "the" if needed
|
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
|
| Thu, 01 Oct 2009 15:19:23 +0200 |
nipkow |
resolved conflict
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 11:35:13 +0200 |
nipkow |
record max lemmas used
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Thu, 24 Sep 2009 17:25:42 +0200 |
nipkow |
record how many "proof"s are solved by s/h
|
file |
diff |
annotate
|
| Sat, 19 Sep 2009 10:19:12 +0200 |
nipkow |
restructured code
|
file |
diff |
annotate
|
| Fri, 18 Sep 2009 23:08:53 +0200 |
nipkow |
modified minimization log
|
file |
diff |
annotate
|
| Fri, 18 Sep 2009 14:40:06 +0200 |
nipkow |
skip &&& goals
|
file |
diff |
annotate
|
| Thu, 17 Sep 2009 19:13:07 +0200 |
nipkow |
removed misleading log line
|
file |
diff |
annotate
|
| Wed, 16 Sep 2009 12:47:14 +0200 |
nipkow |
revised lemma counting
|
file |
diff |
annotate
|
| Tue, 15 Sep 2009 15:29:11 +0200 |
boehmes |
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
|
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
|
| Sun, 13 Sep 2009 02:10:41 +0200 |
wenzelm |
explicitly export type abbreviations (as usual in SML97);
|
file |
diff |
annotate
|
| Sat, 12 Sep 2009 16:30:48 +0200 |
wenzelm |
standard headers and text sections;
|
file |
diff |
annotate
|
| Thu, 10 Sep 2009 15:57:55 +0200 |
nipkow |
position information is now passed to all actions;
|
file |
diff |
annotate
|
| Thu, 10 Sep 2009 12:53:49 +0200 |
nipkow |
logging number of metis lemmas
|
file |
diff |
annotate
|
| Wed, 09 Sep 2009 23:26:34 +0200 |
nipkow |
minimization: comparing w/ and w/o.
|
file |
diff |
annotate
|
| Tue, 08 Sep 2009 09:57:33 +0200 |
boehmes |
timeout option for ATPs
|
file |
diff |
annotate
|
| Mon, 07 Sep 2009 19:41:07 +0200 |
nipkow |
tuned stats
|
file |
diff |
annotate
|
| Mon, 07 Sep 2009 16:24:32 +0200 |
nipkow |
tuned stats
|
file |
diff |
annotate
|
| Mon, 07 Sep 2009 08:32:22 +0200 |
nipkow |
enabled metis permanently, tuned stats
|
file |
diff |
annotate
|
| Sat, 05 Sep 2009 22:01:31 +0200 |
boehmes |
added signature ATP_MINIMAL,
|
file |
diff |
annotate
|
| Sat, 05 Sep 2009 17:34:30 +0200 |
boehmes |
separate output of ATP user time and sledgehammer (ML code) user time
|
file |
diff |
annotate
|
| Sat, 05 Sep 2009 11:45:57 +0200 |
boehmes |
added initialization and cleanup of actions,
|
file |
diff |
annotate
|
| Fri, 04 Sep 2009 13:57:56 +0200 |
boehmes |
tuned
|
file |
diff |
annotate
|
| Thu, 03 Sep 2009 22:47:31 +0200 |
boehmes |
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
|
file |
diff |
annotate
|
| Thu, 03 Sep 2009 18:41:58 +0200 |
boehmes |
added option full_typed for sledgehammer action
|
file |
diff |
annotate
|
| Thu, 03 Sep 2009 17:55:31 +0200 |
boehmes |
added runtime information to sledgehammer
|
file |
diff |
annotate
|
| Thu, 03 Sep 2009 14:05:13 +0200 |
boehmes |
Mirabelle: logging of exceptions (works only for PolyML)
|
file |
diff |
annotate
|
| Wed, 02 Sep 2009 21:31:58 +0200 |
boehmes |
Mirabelle: actions are responsible for handling exceptions,
|
file |
diff |
annotate
|
| Wed, 02 Sep 2009 16:23:53 +0200 |
boehmes |
moved Mirabelle from HOL/Tools to HOL,
|
file |
diff |
annotate
| base
|