| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread through fact triple component from which used facts come, for accurate index output
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
more precise output of selected facts
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
eliminated needless speed optimization -- and simplified code quite a bit
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
|
file |
diff |
annotate
|
| Sun, 13 Jan 2013 22:00:45 +0100 |
blanchet |
more informative output
|
file |
diff |
annotate
|
| Sun, 13 Jan 2013 21:42:39 +0100 |
blanchet |
have Mirabelle produce more output
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 10:54:36 +0100 |
blanchet |
use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 10:41:53 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 19:09:44 +0100 |
blanchet |
added MaSh learning to Mirabelle
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 20:55:33 +0100 |
blanchet |
added "fact_filter" option to Mirabelle
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 12:25:43 +0100 |
smolkas |
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 13:46:24 +0200 |
blanchet |
fixed theorem lookup code in Isar proof reconstruction
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 13:19:44 +0200 |
blanchet |
refactor code
|
file |
diff |
annotate
|
| Tue, 07 Aug 2012 10:28:04 +0200 |
boehmes |
increase defensive timeout that should typically not kick in thanks to solid time limits in Sledgehammer (otherwise, Mirabelle-based evaluations might be distorted)
|
file |
diff |
annotate
|
| Fri, 27 Jul 2012 17:34:33 +0200 |
blanchet |
tweaks in preparation for type encoding evaluation
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
learn from SMT proofs when they can be minimized by Metis
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed ML structures
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
learn from minimized ATP proofs
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
centrally construct expensive data structures
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
more code rationalization in relevance filter
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
systematize lazy names in relevance filter
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
rationalize relevance filter, slowing moving code from Iter to MaSh
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
|
file |
diff |
annotate
|
| Wed, 23 May 2012 21:19:48 +0200 |
blanchet |
improved LEO-II definition handling -- still hoping for a fix directly in LEO-II
|
file |
diff |
annotate
|
| Wed, 23 May 2012 21:19:48 +0200 |
blanchet |
better handling of incomplete TSTP proofs
|
file |
diff |
annotate
|
| Wed, 02 May 2012 11:47:45 +0200 |
wenzelm |
updated headers;
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 14:13:04 +0100 |
sultana |
merged
|
file |
diff |
annotate
| base
|