Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TPTP/MaSh_Export.thy
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
less more (0) tip
isabelle