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
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
Thu, 22 Aug 2013 08:42:27 +0200 blanchet tuning file | diff | annotate
Wed, 21 Aug 2013 16:21:37 +0200 blanchet improve weight computation for complex terms file | diff | annotate
Wed, 21 Aug 2013 15:34:51 +0200 blanchet improved support for MaSh server file | diff | annotate
Wed, 21 Aug 2013 15:18:06 +0200 blanchet get rid of some silly MaSh features 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 take out dangerous feature, now that all updates are permanent file | diff | annotate
Wed, 21 Aug 2013 09:25:40 +0200 blanchet use new MaSh command-line arguments file | diff | annotate
Wed, 21 Aug 2013 09:25:40 +0200 blanchet shutdown MaSh server file | diff | annotate
Tue, 20 Aug 2013 14:36:22 +0200 blanchet adapted ML code to new version of MaSh tool file | diff | annotate
Tue, 20 Aug 2013 14:36:22 +0200 blanchet adapted to new MaSh syntax file | diff | annotate
Tue, 20 Aug 2013 14:36:22 +0200 blanchet tuning file | diff | annotate
Tue, 20 Aug 2013 11:42:52 +0200 blanchet learn MaSh facts on the fly file | diff | annotate
Tue, 20 Aug 2013 11:42:51 +0200 blanchet allow MaSh query to do some learning as well file | diff | annotate
Mon, 19 Aug 2013 23:22:04 +0200 blanchet treat frees as both consts and vars, for more hits file | diff | annotate
Mon, 19 Aug 2013 21:59:36 +0200 blanchet keep long names to stay on the safe side file | diff | annotate
Mon, 19 Aug 2013 18:50:45 +0200 blanchet MaSh tweaking: shorter names + killed (broken) SNoW file | diff | annotate
Mon, 19 Aug 2013 16:50:25 +0200 blanchet handle Bounds as well in MaSh features file | diff | annotate
Mon, 19 Aug 2013 14:47:47 +0200 blanchet add subtypes as well as features in MaSh file | diff | annotate
Mon, 19 Aug 2013 14:41:22 +0200 blanchet generate patterns for variables as well in MaSh (cf. HOL(y)Hammer) file | diff | annotate
Mon, 19 Aug 2013 14:26:59 +0200 blanchet generate deep type patterns in MaSh file | diff | annotate
Thu, 18 Jul 2013 20:53:22 +0200 wenzelm explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it; 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
Sun, 19 May 2013 20:41:19 +0200 blanchet made "completish" mode a bit more complete file | diff | annotate
Fri, 17 May 2013 11:35:52 +0200 wenzelm tuned signature -- emphasize thread creation here; file | diff | annotate
Thu, 16 May 2013 13:34:13 +0200 blanchet tuning -- renamed '_from_' to '_of_' in Sledgehammer file | diff | annotate
Wed, 15 May 2013 17:43:42 +0200 blanchet renamed Sledgehammer functions with 'for' in their names to 'of' file | diff | annotate
Tue, 14 May 2013 20:46:09 +0200 wenzelm more uniform Markup.print_real; file | diff | annotate
Tue, 19 Feb 2013 17:01:06 +0100 blanchet avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs file | diff | annotate
Tue, 19 Feb 2013 13:37:07 +0100 blanchet reintroduced crucial sorting accidentally lost in 962190eab40d file | diff | annotate
Tue, 19 Feb 2013 13:27:33 +0100 blanchet compile 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 18:34:55 +0100 blanchet implement (more) accurate computation of parents file | diff | annotate
Mon, 18 Feb 2013 18:34:54 +0100 blanchet tuning file | diff | annotate
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
less more (0) -100 -60 tip
isabelle