Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TPTP/mash_export.ML
Mon, 08 Sep 2014 13:56:27 +0200 blanchet the kind is now always the empty string -- can no longer distinguish between user theorems and package theorems in a semi-reliable way file | diff | annotate
Wed, 09 Jul 2014 11:35:52 +0200 blanchet tuned terminology file | diff | annotate
Tue, 01 Jul 2014 16:47:10 +0200 blanchet clean up MaSh export a bit file | diff | annotate
Sun, 29 Jun 2014 18:28:27 +0200 blanchet tuning file | diff | annotate
Sun, 29 Jun 2014 18:28:27 +0200 blanchet killed Python version of MaSh, now that the SML version works adequately file | diff | annotate
Fri, 27 Jun 2014 17:18:30 +0200 blanchet use right theory name for theorems in evaluation driver file | diff | annotate
Fri, 27 Jun 2014 17:05:22 +0200 blanchet killed dead code file | diff | annotate
Thu, 26 Jun 2014 20:49:34 +0200 blanchet tuning file | diff | annotate
Thu, 26 Jun 2014 13:33:02 +0200 blanchet avoid parallelism, since it confuses the global state and leads to cheating (with 'sml_xxx' engines) file | diff | annotate
Thu, 26 Jun 2014 13:32:56 +0200 blanchet generate right dependencies in MaSh driver file | diff | annotate
Tue, 24 Jun 2014 15:08:19 +0200 blanchet optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct) file | diff | annotate
Tue, 24 Jun 2014 08:20:00 +0200 blanchet changed order of facts so that 'name_tabs' has the same order everywhere (which affects unaliasing) file | diff | annotate
Mon, 02 Jun 2014 11:59:50 +0200 blanchet add option to keep duplicates, for more precise evaluation of relevance filters file | diff | annotate
Fri, 30 May 2014 12:27:51 +0200 blanchet added another way of invoking Python code, for experiments file | diff | annotate
Fri, 30 May 2014 12:27:51 +0200 blanchet more work on exporter file | diff | annotate
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, 23 May 2014 14:12:21 +0200 blanchet fixed semantics of 'linearize' file | diff | annotate
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
less more (0) -100 -60 tip
isabelle