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/Tools/Sledgehammer/sledgehammer_mash.ML
Mon, 18 Feb 2013 11:33:43 +0100 blanchet tuned code: factored out parent computation file | diff | annotate
Mon, 18 Feb 2013 10:43:36 +0100 blanchet tuned code file | diff | annotate
Fri, 15 Feb 2013 09:17:20 +0100 blanchet avoid crude/wrong theorem comparision file | diff | annotate
Fri, 15 Feb 2013 09:17:20 +0100 blanchet tuned code file | diff | annotate
Fri, 15 Feb 2013 09:17:20 +0100 blanchet more MaSh tracing file | diff | annotate
Fri, 15 Feb 2013 09:17:20 +0100 blanchet tuning file | diff | annotate
Fri, 08 Feb 2013 12:22:37 +0100 blanchet added option to use SNoW as machine learning algo file | diff | annotate
Thu, 07 Feb 2013 14:05:33 +0100 blanchet killed deadcode file | diff | annotate
Thu, 07 Feb 2013 14:05:32 +0100 blanchet drop needless .0s file | diff | annotate
Thu, 07 Feb 2013 14:05:32 +0100 blanchet distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation file | diff | annotate
Tue, 05 Feb 2013 17:19:13 +0100 blanchet removed spurious trimming file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet tuned data structure file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet more precise output of selected facts file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet eliminated needless speed optimization -- and simplified code quite a bit file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices file | diff | annotate
Thu, 31 Jan 2013 12:09:07 +0100 blanchet adapted to new MaSh interface file | diff | annotate
Sat, 19 Jan 2013 17:42:12 +0100 blanchet tuning file | diff | annotate
Fri, 18 Jan 2013 16:06:45 +0100 blanchet tuning file | diff | annotate
Fri, 18 Jan 2013 00:18:11 +0100 blanchet optimization -- evaluate conversion to table only once 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 18:43:59 +0100 blanchet evaluate more cases (cf. paper) file | diff | annotate
Thu, 17 Jan 2013 17:55:03 +0100 blanchet updated MaSh file | diff | annotate
Mon, 14 Jan 2013 09:59:50 +0100 blanchet adjust weights -- sorts are prolific, so tone them down even more file | diff | annotate
Sun, 13 Jan 2013 22:17:00 +0100 blanchet don't learn theories -- this option is very slow and not very helpful file | diff | annotate
Sun, 13 Jan 2013 20:57:48 +0100 blanchet honor unknown chained in MaSh and a few other tweaks file | diff | annotate
Sun, 13 Jan 2013 15:04:55 +0100 blanchet remove obsolete MaSh files file | diff | annotate
Sun, 13 Jan 2013 12:15:44 +0100 blanchet cleaned up hint handling file | diff | annotate
Sun, 13 Jan 2013 12:15:43 +0100 blanchet better handlig of built-ins -- at the top-level, not in subterms file | diff | annotate
Sat, 12 Jan 2013 16:49:40 +0100 blanchet honor filtering out of arguments for built-in constants (e.g. representation of numerals) file | diff | annotate
Sat, 12 Jan 2013 16:49:39 +0100 blanchet new version of MaSh Python component file | diff | annotate
Fri, 11 Jan 2013 16:30:56 +0100 blanchet don't learn from the proof of "psimps" etc. file | diff | annotate
Fri, 11 Jan 2013 16:30:56 +0100 blanchet updated MaSh Python component file | diff | annotate
Fri, 11 Jan 2013 16:30:56 +0100 blanchet start using MaSh hints file | diff | annotate
Fri, 11 Jan 2013 16:30:56 +0100 blanchet always compare theorem using the same, weaker function 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 get rid of spurious "Isar" proofs 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
Sat, 05 Jan 2013 22:31:33 +0100 blanchet tuned message file | diff | annotate
Sat, 05 Jan 2013 22:31:32 +0100 blanchet tap after, not before command invocation file | diff | annotate
Fri, 04 Jan 2013 21:56:20 +0100 blanchet refined class handling, to prevent cycles in fact graph file | diff | annotate
Fri, 04 Jan 2013 21:56:19 +0100 blanchet tweaked nicknames file | diff | annotate
Fri, 04 Jan 2013 19:00:49 +0100 blanchet speed up generation of local theorem nicknames file | diff | annotate
Fri, 04 Jan 2013 19:00:49 +0100 blanchet tweaked fudge factor file | diff | annotate
Wed, 02 Jan 2013 10:41:53 +0100 blanchet tuning file | diff | annotate
Fri, 28 Dec 2012 23:31:51 +0100 blanchet tuned ML function name file | diff | annotate
Fri, 28 Dec 2012 21:03:39 +0100 blanchet slightly more elegant naming convention (to keep low-level and high-level APIs separated) file | diff | annotate
Fri, 28 Dec 2012 14:13:39 +0100 blanchet tuned ML function names 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
Thu, 27 Dec 2012 15:46:27 +0100 blanchet enable theory learning in MaSh file | diff | annotate
Fri, 21 Dec 2012 14:35:29 +0100 blanchet name tuning file | diff | annotate
Thu, 20 Dec 2012 15:51:27 +0100 blanchet better weight functions for MePo/MaSh etc. file | diff | annotate
Mon, 17 Dec 2012 22:09:48 +0100 blanchet updated MaSh serialization number (to reflect new weights) file | diff | annotate
Mon, 17 Dec 2012 22:06:28 +0100 blanchet contain exponential explosion of term patterns file | diff | annotate
Mon, 17 Dec 2012 22:06:28 +0100 blanchet tuned weights -- keep same relative values, but use 1.0 as the least weight file | diff | annotate
Mon, 17 Dec 2012 22:06:28 +0100 blanchet really honor pattern depth, and use 2 by default file | diff | annotate
Sun, 16 Dec 2012 19:23:04 +0100 blanchet tuning file | diff | annotate
Sat, 15 Dec 2012 19:57:12 +0100 blanchet thread no timeout properly 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
less more (0) -100 -60 tip
isabelle