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.ML
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
Wed, 11 Jul 2012 21:43:19 +0200 blanchet generate ATP dependencies file | diff | annotate
Wed, 11 Jul 2012 11:28:27 +0200 blanchet comment file | diff | annotate
Wed, 11 Jul 2012 09:32:29 +0200 blanchet rationalized output 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