Mon, 17 May 2010 15:11:25 +0200 |
wenzelm |
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
|
file |
diff |
annotate
|
Sun, 16 May 2010 00:02:11 +0200 |
wenzelm |
prefer structure Parse_Spec;
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 16:56:03 +0200 |
blanchet |
make Mirabelle happy
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 21:50:36 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
Fri, 23 Apr 2010 16:55:51 +0200 |
blanchet |
move some sledgehammer stuff out of "atp_manager.ML"
|
file |
diff |
annotate
|
Fri, 23 Apr 2010 12:24:30 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
Mon, 19 Apr 2010 15:15:21 +0200 |
blanchet |
make Sledgehammer's minimizer also minimize Isar proofs
|
file |
diff |
annotate
|
Thu, 01 Apr 2010 11:12:08 +0200 |
blanchet |
add missing goal argument
|
file |
diff |
annotate
|
Thu, 25 Mar 2010 17:55:55 +0100 |
blanchet |
make Mirabelle happy again
|
file |
diff |
annotate
|
Mon, 22 Mar 2010 10:38:28 +0100 |
blanchet |
remove the iteration counter from Sledgehammer's minimizer
|
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
|
Thu, 18 Mar 2010 13:43:50 +0100 |
blanchet |
fix Mirabelle after renaming 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, 10 Dec 2009 18:10:59 +0100 |
boehmes |
only invoke metisFT if metis failed
|
file |
diff |
annotate
|
Tue, 08 Dec 2009 23:05:23 +0100 |
boehmes |
also consider the fully-typed version of metis for Mirabelle measurements
|
file |
diff |
annotate
|
Thu, 29 Oct 2009 16:59:12 +0100 |
wenzelm |
modernized some structure names;
|
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 18:00:50 +0100 |
boehmes |
measure runtime of ATPs only if requested
|
file |
diff |
annotate
|
Tue, 20 Oct 2009 12:06:17 +0200 |
boehmes |
proper exceptions instead of unhandled partiality
|
file |
diff |
annotate
|
Sun, 18 Oct 2009 16:25:59 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
Sun, 18 Oct 2009 16:25:04 +0200 |
nipkow |
added sums of squares for standard deviation
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 23:47:27 +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 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
|