| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 13:56:28 +0200 |
blanchet |
refactored MaSh files to avoid regenerating exports on each eval
|
file |
diff |
annotate
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
clean up MaSh export a bit
|
file |
diff |
annotate
|
| Sun, 29 Jun 2014 18:28:27 +0200 |
blanchet |
killed Python version of MaSh, now that the SML version works adequately
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 11:59:50 +0200 |
blanchet |
add option to keep duplicates, for more precise evaluation of relevance filters
|
file |
diff |
annotate
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
more work on exporter
|
file |
diff |
annotate
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
got rid of 'linearize' option
|
file |
diff |
annotate
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
extend exporter with new versions of MaSh
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 16:10:39 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 13:42:47 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
tuned ML file name
|
file |
diff |
annotate
|
| Wed, 11 Dec 2013 18:02:22 +0100 |
wenzelm |
support for polml-5.5.2;
|
file |
diff |
annotate
|
| Tue, 15 Oct 2013 23:00:46 +0200 |
blanchet |
tweaked signature
|
file |
diff |
annotate
|
| Wed, 21 Aug 2013 09:25:40 +0200 |
blanchet |
generate max suggestions in MaSh export driver
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 13:21:49 +0100 |
blanchet |
provide two modes for MaSh driver: linearized or real visibility
|
file |
diff |
annotate
|
| Thu, 07 Feb 2013 14:05:33 +0100 |
blanchet |
hide "ext" name, but keep "HOL.ext", to ensure consistency in naming when "ext" is used by LEO-II or Satallax implicitly
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 23:53:55 +0100 |
blanchet |
MeSh prover generation
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 23:29:17 +0100 |
blanchet |
use precomputed MaSh/MePo data whenever available
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 19:20:56 +0100 |
blanchet |
added step to skip some queries
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 13:11:44 +0100 |
blanchet |
tweaked defaults
|
file |
diff |
annotate
|
| Wed, 16 Jan 2013 12:46:11 +0100 |
blanchet |
honor fact range for MePo as well
|
file |
diff |
annotate
|
| Thu, 10 Jan 2013 23:48:01 +0100 |
blanchet |
removed debugging code
|
file |
diff |
annotate
|
| Thu, 10 Jan 2013 23:34:19 +0100 |
blanchet |
export MeSh data as well
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 21:34:32 +0100 |
blanchet |
MaSh exporter can now export subsets of the facts, as consecutive ranges
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 22:49:06 +0100 |
blanchet |
parallelized MaSh exporter
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 21:59:03 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 00:24:06 +0100 |
blanchet |
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 00:48:50 +0100 |
blanchet |
more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 16:49:48 +0100 |
blanchet |
export ATP and Isar commands separately
|
file |
diff |
annotate
|