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_eval.ML
Fri, 09 Jul 2021 17:58:17 +0200 desharna fixed HOL-TPTP following f58108b7a60c file | diff | annotate
Sun, 14 Aug 2016 12:26:09 +0200 blanchet killed final stops in Sledgehammer and friends file | diff | annotate
Sun, 04 Oct 2015 17:41:52 +0200 blanchet sped up MaSh nickname generation file | diff | annotate
Fri, 03 Jul 2015 16:19:45 +0200 wenzelm clarified context; file | diff | annotate
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2}; file | diff | annotate
Thu, 06 Nov 2014 15:42:34 +0100 wenzelm proper Keyword.keywords (cf. 82a71046dce8); file | diff | annotate
Mon, 08 Sep 2014 13:56:27 +0200 blanchet added missing 'transpose' file | diff | annotate
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT' file | diff | annotate
Tue, 01 Jul 2014 16:47:10 +0200 blanchet clean up MaSh evaluation driver file | diff | annotate
Sun, 29 Jun 2014 18:30:24 +0200 blanchet use SMT2 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:05:22 +0200 blanchet killed dead code 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
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
Wed, 28 May 2014 17:42:36 +0200 blanchet more generous max number of suggestions, for more safety file | diff | annotate
Fri, 31 Jan 2014 16:10:39 +0100 blanchet tuning file | diff | annotate
Fri, 31 Jan 2014 12:30:54 +0100 blanchet refactor large ML file file | diff | annotate
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed ML file file | diff | annotate
Fri, 31 Jan 2014 10:23:32 +0100 blanchet tuned ML file name file | diff | annotate
Thu, 19 Dec 2013 13:43:21 +0100 blanchet made timeouts in Sledgehammer not be 'option's -- simplified lots of code file | diff | annotate
Thu, 17 Oct 2013 20:49:19 +0200 blanchet generate a comment storing the goal nickname in "learn_prover" file | diff | annotate
Sun, 29 Sep 2013 12:21:11 +0200 wenzelm made SML/NJ happy (NB: toplevel ML environment is unmanaged); file | diff | annotate
Thu, 22 Aug 2013 12:12:51 +0200 blanchet cleanup old duplicated functionality 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
Thu, 16 May 2013 13:34:13 +0200 blanchet tuning -- renamed '_from_' to '_of_' in Sledgehammer file | diff | annotate
Wed, 20 Feb 2013 13:04:03 +0100 blanchet honor linearization option also in the evaluation driver 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
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
Thu, 07 Feb 2013 14:05:33 +0100 blanchet more robustness w.r.t. 0 file | diff | annotate
Thu, 31 Jan 2013 18:04:19 +0100 blanchet compile 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 distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds 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 23:29:17 +0100 blanchet use precomputed MaSh/MePo data whenever available file | diff | annotate
Thu, 17 Jan 2013 18:53:13 +0100 blanchet provide a means to skip a method file | diff | annotate
Thu, 17 Jan 2013 18:43:59 +0100 blanchet evaluate more cases (cf. paper) 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
Tue, 08 Jan 2013 13:16:39 +0100 blanchet tuned output 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
Fri, 28 Dec 2012 23:31:51 +0100 blanchet tuned ML function name 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 10:21:21 +0100 blanchet fixed total file | diff | annotate
Tue, 18 Dec 2012 02:19:14 +0100 blanchet avoid references altogether file | diff | annotate
Tue, 18 Dec 2012 00:17:37 +0100 blanchet no need for tracing file | diff | annotate
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
less more (0) -100 -60 tip
isabelle