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
Thu, 22 May 2014 04:12:06 +0200 blanchet reverted '|' features in MaSh -- these sounded like a good idea but never really worked file | diff | annotate
Mon, 19 May 2014 23:43:53 +0200 blanchet store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution file | diff | annotate
Fri, 31 Jan 2014 16:10:39 +0100 blanchet tuning file | diff | annotate
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed ML file file | diff | annotate
Mon, 09 Dec 2013 04:03:30 +0100 blanchet generate problems with type classes file | diff | annotate
Fri, 18 Oct 2013 00:05:31 +0200 blanchet make sure add: doesn't add duplicates, and works for [no_atp] facts file | diff | annotate
Tue, 15 Oct 2013 23:00:46 +0200 blanchet tweaked signature file | diff | annotate
Thu, 10 Oct 2013 01:17:37 +0200 blanchet simplify fudge factor code file | diff | annotate
Wed, 09 Oct 2013 15:39:34 +0200 blanchet use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected) file | diff | annotate
Wed, 09 Oct 2013 09:47:59 +0200 blanchet optimized built-in const check file | diff | annotate
Fri, 23 Aug 2013 16:51:53 +0200 blanchet repaired num_extra_feature_facts + tuning file | diff | annotate
Thu, 22 Aug 2013 12:16:56 +0200 blanchet take chained and proximate facts into consideration when computing MaSh features file | diff | annotate
Thu, 22 Aug 2013 12:12:52 +0200 blanchet pour extra features from proximate facts into goal, in exporter file | diff | annotate
Wed, 21 Aug 2013 14:54:25 +0200 blanchet weight MaSh constants by frequency file | diff | annotate
Wed, 21 Aug 2013 09:25:40 +0200 blanchet only generate feature weights for queries -- they're not used elsewhere file | diff | annotate
Wed, 21 Aug 2013 09:25:40 +0200 blanchet generate max suggestions in MaSh export driver file | diff | annotate
Tue, 28 May 2013 08:52:41 +0200 blanchet redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e]) file | diff | annotate
Fri, 24 May 2013 16:43:37 +0200 blanchet improved handling of free variables' types in Isar proofs 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
Mon, 18 Feb 2013 11:33:43 +0100 blanchet tuned code: factored out parent computation file | diff | annotate
Fri, 15 Feb 2013 09:17:20 +0100 blanchet tuned code file | diff | annotate
Fri, 08 Feb 2013 16:41:04 +0100 blanchet distinguish one more kind of proofs file | diff | annotate
Fri, 08 Feb 2013 15:38:33 +0100 blanchet added markers in proofs identifying origin of proofs, in eval driver file | diff | annotate
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
less more (0) -60 tip
isabelle