Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TPTP/mash_export.ML
Tue, 05 Feb 2013 17:19:13 +0100 blanchet removed spurious trimming file | diff | annotate
Thu, 17 Jan 2013 23:29:22 +0100 blanchet use correct weights in MeSh driver file | diff | annotate
Thu, 17 Jan 2013 19:20:56 +0100 blanchet added step to skip some queries file | diff | annotate
Wed, 16 Jan 2013 12:55:29 +0100 blanchet graceful failure file | diff | annotate
Wed, 16 Jan 2013 12:46:11 +0100 blanchet honor fact range for MePo as well file | diff | annotate
Sun, 13 Jan 2013 12:28:20 +0100 blanchet don't generate queries with empty dependency list file | diff | annotate
Fri, 11 Jan 2013 16:30:56 +0100 blanchet fixed escaping for MeSh encoder file | diff | annotate
Fri, 11 Jan 2013 16:30:56 +0100 blanchet start using MaSh hints file | diff | annotate
Thu, 10 Jan 2013 23:34:19 +0100 blanchet export MeSh data as well file | diff | annotate
Sun, 06 Jan 2013 17:38:29 +0100 blanchet also generate queries for goals with too many Isar dependencies file | diff | annotate
Fri, 04 Jan 2013 21:56:20 +0100 blanchet refined class handling, to prevent cycles in fact graph file | diff | annotate
Thu, 27 Dec 2012 16:49:12 +0100 blanchet improved thm order hack, in case the default names are overridden file | diff | annotate
Fri, 21 Dec 2012 15:22:57 +0100 blanchet linearize eval driver, to work around horrible bug in previous implementation file | diff | annotate
Mon, 17 Dec 2012 22:06:28 +0100 blanchet tuned order to help debugging file | diff | annotate
Sun, 16 Dec 2012 12:07:37 +0100 blanchet added tracing to ATP exporter 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 23:47:01 +0100 blanchet get rid of some junk facts in the MaSh evaluation driver file | diff | annotate
Thu, 13 Dec 2012 22:49:06 +0100 blanchet parallelized MaSh exporter file | diff | annotate
Thu, 13 Dec 2012 09:21:45 +0100 blanchet shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other file | diff | annotate
Wed, 12 Dec 2012 21:48:29 +0100 blanchet don't query blacklisted theorems in evaluation driver file | diff | annotate
Wed, 12 Dec 2012 02:47:45 +0100 blanchet merge aliased theorems in MaSh dependencies, modulo symmetry of equality 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 21:54:28 +0100 blanchet don't blacklist "case" theorems -- this causes problems in MaSh later 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
Thu, 06 Dec 2012 16:07:09 +0100 blanchet use right names in MePo exporter file | diff | annotate
Tue, 04 Dec 2012 23:19:03 +0100 blanchet added feature weights in MaSh file | diff | annotate
Tue, 04 Dec 2012 18:12:29 +0100 blanchet generalized MaSh exporter to sets of theories file | diff | annotate
Fri, 03 Aug 2012 17:56:35 +0200 blanchet rule out same "technical" theories for MePo as for MaSh file | diff | annotate
Fri, 03 Aug 2012 17:56:35 +0200 blanchet don't generate queries for empty dependencies file | diff | annotate
Fri, 03 Aug 2012 17:56:35 +0200 blanchet crank up max number of dependencies 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 repaired accessibility chains generated by MaSh exporter + tuned one function out 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 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet honor suggested MaSh weights file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet relearn ATP proofs file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet added "learn_from_atp" command to MaSh, for patient users file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet added locality as a MaSh feature file | diff | annotate
Fri, 20 Jul 2012 22:19:45 +0200 blanchet renamed ML structures file | diff | annotate
Fri, 20 Jul 2012 22:19:45 +0200 blanchet renamed "iter" fact filter to "MePo" (Meng--Paulson) file | diff | annotate
Fri, 20 Jul 2012 22:19:45 +0200 blanchet handle local facts smoothly in MaSh 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 speed up tautology/metaness check 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:04 +0200 blanchet more consolidation of MaSh code file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet drastic overhaul of MaSh data structures + fixed a few performance issues file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet fixed order of accessibles + other tweaks to MaSh 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:04 +0200 blanchet improved MaSh string escaping and make more operations string-based file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet more implementation work on MaSh file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet tweak output 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 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, 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
less more (0) -60 tip
isabelle