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/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
Thu, 06 Nov 2014 15:05:15 +0100 wenzelm prefer explicit Keyword.keywords (cf. 82a71046dce8); file | diff | annotate
Mon, 02 Jun 2014 15:10:18 +0200 fleury basic setup for zipperposition prover 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
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
Thu, 17 Oct 2013 01:22:15 +0200 blanchet tuning file | diff | annotate
Thu, 17 Oct 2013 01:10:08 +0200 blanchet if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice file | diff | annotate
Thu, 10 Oct 2013 01:17:37 +0200 blanchet simplify fudge factor code file | diff | annotate
Wed, 11 Sep 2013 22:20:45 +0200 blanchet killed dead code 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
Wed, 15 May 2013 17:49:18 +0200 blanchet compile file | diff | annotate
Tue, 14 May 2013 19:48:31 +0200 wenzelm more uniform Markup.parse_real; 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, 20 Jul 2012 22:19:46 +0200 blanchet honor suggested MaSh weights file | diff | annotate
Fri, 20 Jul 2012 22:19:45 +0200 blanchet renamed ML structures file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet centrally construct expensive data structures file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet renamed Sledgehammer options file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet more code rationalization in relevance filter file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet systematize lazy names in relevance filter file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet rationalize relevance filter, slowing moving code from Iter to MaSh file | diff | annotate
Wed, 11 Jul 2012 21:43:19 +0200 blanchet further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer) file | diff | annotate
Wed, 02 May 2012 11:47:45 +0200 wenzelm updated headers; file | diff | annotate
Tue, 24 Apr 2012 13:59:29 +0100 sultana reversed Tools to Actions Mirabelle renaming; file | diff | annotate | base
Thu, 01 Dec 2011 13:34:13 +0100 blanchet renamed "slicing" to "slice" file | diff | annotate
Wed, 31 Aug 2011 11:52:03 +0200 blanchet more tuning file | diff | annotate
Tue, 30 Aug 2011 14:12:55 +0200 nik improved handling of induction rules in Sledgehammer file | diff | annotate
Fri, 08 Jul 2011 17:04:38 +0200 wenzelm discontinued odd Position.column -- left-over from attempts at PGIP implementation; file | diff | annotate
Fri, 10 Jun 2011 12:01:15 +0200 blanchet compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time file | diff | annotate
Tue, 31 May 2011 16:38:36 +0200 blanchet compile file | diff | annotate
Fri, 27 May 2011 10:30:07 +0200 blanchet fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context file | diff | annotate
Tue, 24 May 2011 00:01:33 +0200 blanchet tuning -- the "appropriate" terminology is inspired from TPTP file | diff | annotate
Sun, 22 May 2011 14:51:42 +0200 blanchet improved Waldmeister support -- even run it by default on unit equational goals file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet remove unused parameter file | diff | annotate
Thu, 12 May 2011 15:29:19 +0200 blanchet fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized file | diff | annotate
Mon, 02 May 2011 22:52:15 +0200 blanchet tuning file | diff | annotate
Mon, 02 May 2011 22:52:15 +0200 blanchet have each ATP filter out dangerous facts for themselves, based on their type system file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags" file | diff | annotate
Sun, 01 May 2011 18:37:25 +0200 blanchet implement the new ATP type system in Sledgehammer file | diff | annotate
Thu, 21 Apr 2011 22:18:28 +0200 blanchet detect some unsound proofs before showing them to the user file | diff | annotate
Thu, 21 Apr 2011 18:39:22 +0200 blanchet implemented general slicing for ATPs, especially E 1.2w and above file | diff | annotate
Mon, 21 Feb 2011 10:31:48 +0100 blanchet give more weight to Frees than to Consts in relevance filter file | diff | annotate
Fri, 07 Jan 2011 23:07:04 +0100 wenzelm tuned; file | diff | annotate
Wed, 29 Dec 2010 12:16:49 +0100 wenzelm made SML/NJ happy; file | diff | annotate
Wed, 15 Dec 2010 12:08:41 +0100 blanchet honor "overlord" option for SMT solvers as well and don't pass "ext" to them file | diff | annotate
Wed, 15 Dec 2010 11:26:28 +0100 blanchet implemented partially-typed "tags" type encoding file | diff | annotate
Wed, 08 Dec 2010 22:17:52 +0100 blanchet split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems file | diff | annotate
Fri, 03 Dec 2010 18:29:14 +0100 blanchet replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us file | diff | annotate
Thu, 04 Nov 2010 14:59:44 +0100 blanchet use the SMT integration's official list of built-ins file | diff | annotate
Wed, 27 Oct 2010 09:22:40 +0200 blanchet generalize to handle any prover (not just E) file | diff | annotate
Fri, 22 Oct 2010 15:02:27 +0200 blanchet generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different) file | diff | annotate
Fri, 22 Oct 2010 14:47:43 +0200 blanchet replaced references with proper record that's threaded through file | diff | annotate
Fri, 22 Oct 2010 14:10:32 +0200 blanchet fixed signature of "is_smt_solver_installed"; file | diff | annotate
Wed, 01 Sep 2010 17:27:10 +0200 blanchet got rid of the "theory_relevant" option; file | diff | annotate
Wed, 01 Sep 2010 16:11:48 +0200 blanchet support new option in Mirabelle file | diff | annotate
Wed, 01 Sep 2010 10:26:54 +0200 blanchet introduce fudge factors to deal with "theory const" file | diff | annotate
Tue, 31 Aug 2010 23:50:59 +0200 blanchet finished renaming file | diff | annotate
Tue, 31 Aug 2010 20:23:32 +0200 blanchet add one option to Mirabelle file | diff | annotate
less more (0) -60 tip
isabelle