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/Mirabelle/Tools/mirabelle_sledgehammer.ML
Fri, 01 Aug 2014 14:43:57 +0200 blanchet modernized Mirabelle (a bit) and made it compile file | diff | annotate
Mon, 02 Jun 2014 15:10:18 +0200 fleury basic setup for zipperposition prover file | diff | annotate
Thu, 01 May 2014 09:30:35 +0200 haftmann optional case enforcement file | diff | annotate
Fri, 04 Apr 2014 19:09:56 +0200 blanchet added option to Mirabelle file | diff | annotate
Mon, 03 Feb 2014 16:53:58 +0100 blanchet renamed ML file file | diff | annotate
Mon, 03 Feb 2014 15:19:07 +0100 blanchet merged 'reconstructors' and 'proof methods' file | diff | annotate
Fri, 31 Jan 2014 16:10:39 +0100 blanchet tuning file | diff | annotate
Fri, 31 Jan 2014 16:07:20 +0100 blanchet moved ML code around file | diff | annotate
Fri, 31 Jan 2014 13:42:47 +0100 blanchet compile 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 many Sledgehammer ML files to clarify structure 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 17:52:58 +0100 blanchet refactored preplaying outcome data structure file | diff | annotate
Thu, 19 Dec 2013 09:28:20 +0100 blanchet tuning file | diff | annotate
Tue, 19 Nov 2013 18:34:04 +0100 blanchet tuning file | diff | annotate
Tue, 19 Nov 2013 17:37:35 +0100 blanchet refactoring 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
Thu, 17 Oct 2013 02:22:54 +0200 blanchet thread the goal through instead of relying on unreliable (possibly fake) state 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
Mon, 19 Aug 2013 12:05:33 +0200 blanchet improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success file | diff | annotate
Tue, 09 Jul 2013 18:44:59 +0200 smolkas moved code -> easier debugging 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
Sun, 12 May 2013 20:46:17 +0200 wenzelm more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString; file | diff | annotate
Wed, 20 Feb 2013 17:15:06 +0100 blanchet tweaked hack some more file | diff | annotate
Wed, 20 Feb 2013 15:43:51 +0100 blanchet improved hack file | diff | annotate
Wed, 20 Feb 2013 14:47:19 +0100 blanchet trust preplayed proof in Mirabelle 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
Thu, 31 Jan 2013 17:54:05 +0100 blanchet tuned data structure file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet thread through fact triple component from which used facts come, for accurate index output 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
Sun, 13 Jan 2013 22:00:45 +0100 blanchet more informative output file | diff | annotate
Sun, 13 Jan 2013 21:42:39 +0100 blanchet have Mirabelle produce more output file | diff | annotate
Wed, 02 Jan 2013 10:54:36 +0100 blanchet use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most) file | diff | annotate
Wed, 02 Jan 2013 10:41:53 +0100 blanchet tuning file | diff | annotate
Tue, 04 Dec 2012 19:09:44 +0100 blanchet added MaSh learning to Mirabelle file | diff | annotate
Mon, 03 Dec 2012 20:55:33 +0100 blanchet added "fact_filter" option to Mirabelle file | diff | annotate
Wed, 28 Nov 2012 12:25:43 +0100 smolkas moved thms_of_name to Sledgehammer_Util and removed copies, updated references file | diff | annotate
Thu, 18 Oct 2012 13:46:24 +0200 blanchet fixed theorem lookup code in Isar proof reconstruction file | diff | annotate
Thu, 18 Oct 2012 13:19:44 +0200 blanchet refactor code file | diff | annotate
Tue, 07 Aug 2012 10:28:04 +0200 boehmes increase defensive timeout that should typically not kick in thanks to solid time limits in Sledgehammer (otherwise, Mirabelle-based evaluations might be distorted) file | diff | annotate
Fri, 27 Jul 2012 17:34:33 +0200 blanchet tweaks in preparation for type encoding evaluation file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet learn from SMT proofs when they can be minimized by Metis file | diff | annotate
Fri, 20 Jul 2012 22:19:45 +0200 blanchet renamed ML structures file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet learn from minimized ATP proofs 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, 23 May 2012 21:19:48 +0200 blanchet improved LEO-II definition handling -- still hoping for a fix directly in LEO-II file | diff | annotate
Wed, 23 May 2012 21:19:48 +0200 blanchet better handling of incomplete TSTP proofs file | diff | annotate
less more (0) -100 -60 tip
isabelle