| 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
|
| Tue, 04 Dec 2012 18:12:30 +0100 |
blanchet |
tuned MaSh exporter -- and don't make temp directories unless explicitly told so
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 18:12:29 +0100 |
blanchet |
generalized MaSh exporter to sets of theories
|
file |
diff |
annotate
|
| Mon, 03 Dec 2012 23:43:52 +0100 |
blanchet |
tweaked MaSh exporter
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 10:48:03 +0200 |
blanchet |
don't export technical theorems for MaSh
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 10:48:03 +0200 |
blanchet |
generate fact name in queries again + use ATP dependencies when possible
|
file |
diff |
annotate
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed "iter" fact filter to "MePo" (Meng--Paulson)
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:05 +0200 |
blanchet |
repair MaSh exporter
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
more work on MaSh
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
started implementing MaSh client-side I/O
|
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 |
gracefully handle the case of empty theories when going up the accessibility chain
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
dependency tuning
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
moved most of MaSh exporter code to Sledgehammer
|
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, 11 Jul 2012 21:43:19 +0200 |
blanchet |
add Isabelle dependencies to tweak relevance filter
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
generate ATP dependencies
|
file |
diff |
annotate
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
generate Meng--Paulson facts for evaluation purposes
|
file |
diff |
annotate
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
MaSh evaluation driver
|
file |
diff |
annotate
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
moved MaSh into own files
|
file |
diff |
annotate
|