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_eval.ML
Mon, 17 Dec 2012 22:06:28 +0100 blanchet synchronize access to shared reference and print proper total file | diff | annotate
Sun, 16 Dec 2012 14:19:08 +0100 blanchet escape nicknames file | diff | annotate
Sun, 16 Dec 2012 12:07:56 +0100 blanchet generate proper nicks also for instantiated induction rules 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
Sat, 15 Dec 2012 19:57:12 +0100 blanchet thread no timeout properly file | diff | annotate
Sat, 15 Dec 2012 18:48:58 +0100 blanchet proper escaping in file name file | diff | annotate
Sat, 15 Dec 2012 18:26:37 +0100 blanchet encode lemma name in file name file | diff | annotate
Thu, 13 Dec 2012 22:49:07 +0100 blanchet use MaSh nicknames in ATP problem files to facilitate gathering of statistics 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:14:58 +0100 blanchet better name for SMT solver files file | diff | annotate
Mon, 10 Dec 2012 13:33:06 +0100 blanchet changed capitalization of MeSh filter file | diff | annotate
Mon, 10 Dec 2012 13:02:56 +0100 blanchet (re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores file | diff | annotate
Mon, 10 Dec 2012 10:29:52 +0100 blanchet have MaSh evaluator keep all raw problem/solution files in a directory 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:51 +0100 blanchet don't have MaSh pretend it knows facts it doesn't know file | diff | annotate
Sat, 08 Dec 2012 00:48:51 +0100 blanchet reverted parallel map idea -- appears to make success rate of ATPs less stable (might even lead to bias in favor of MePo) file | diff | annotate
Sat, 08 Dec 2012 00:48:50 +0100 blanchet store evaluation output in a file file | diff | annotate
Sat, 08 Dec 2012 00:48:50 +0100 blanchet use parallel map file | diff | annotate
Thu, 06 Dec 2012 17:48:04 +0100 blanchet use proper entry point for MaSh in test driver file | diff | annotate
Wed, 05 Dec 2012 13:25:06 +0100 blanchet take proximity into account for MaSh + fix a debilitating bug in feature generation file | diff | annotate
Tue, 04 Dec 2012 23:50:36 +0100 blanchet rationalized MaSh evaluation harness file | diff | annotate
Tue, 31 Jul 2012 14:42:03 +0200 wenzelm made SML/NJ happy; 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
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: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 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case) 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 mesh facts by taking into consideration whether a fact is known to MeSh file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet implemented meshing of Iter and MaSh results file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet implemented MaSh QUERY operation file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet cleaner handling of metacharacters + freshness of one-off facts 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 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 more work on MaSh file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet renamed Sledgehammer options 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, 18 Jul 2012 08:44:03 +0200 blanchet renaming file | diff | annotate | base
less more (0) tip
isabelle