src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
Sat, 24 Jan 2015 21:36:21 +0100 wenzelm tuned message;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Fri, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
Thu, 06 Nov 2014 13:36:19 +0100 wenzelm prefer explicit Keyword.keywords;
Wed, 05 Nov 2014 20:49:30 +0100 wenzelm eliminated pointless dynamic keywords (TTY legacy);
Wed, 05 Nov 2014 20:20:57 +0100 wenzelm explicit type Keyword.keywords;
Sat, 01 Nov 2014 19:33:51 +0100 wenzelm recover via scanner;
Sat, 01 Nov 2014 18:46:48 +0100 wenzelm simplified -- scanning is never interactive;
Wed, 08 Oct 2014 17:09:07 +0200 wenzelm added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
Thu, 21 Aug 2014 22:48:39 +0200 wenzelm tuned signature -- define some elementary operations earlier;
Sun, 10 Aug 2014 14:34:43 +0200 wenzelm merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
Fri, 01 Aug 2014 15:08:49 +0200 blanchet careful when calling 'Thm.proof_body_of' -- it can throw exceptions
Fri, 01 Aug 2014 16:07:33 +0200 blanchet peek instead of joining -- is perhaps less risky
Fri, 01 Aug 2014 14:43:57 +0200 blanchet generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
Tue, 24 Jun 2014 15:08:19 +0200 blanchet optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
Wed, 28 May 2014 17:42:36 +0200 blanchet more generous max number of suggestions, for more safety
Thu, 22 May 2014 04:12:06 +0200 blanchet reverted '|' features in MaSh -- these sounded like a good idea but never really worked
Mon, 03 Feb 2014 15:19:07 +0100 blanchet merged 'reconstructors' and 'proof methods'
Fri, 31 Jan 2014 19:16:41 +0100 blanchet generalized preplaying infrastructure to store various results for various methods
Fri, 31 Jan 2014 16:10:39 +0100 blanchet tuning
Thu, 19 Dec 2013 16:11:20 +0100 blanchet tuning
Thu, 19 Dec 2013 13:43:21 +0100 blanchet made timeouts in Sledgehammer not be 'option's -- simplified lots of code
Mon, 09 Dec 2013 04:03:30 +0100 blanchet generate problems with type classes
Tue, 15 Oct 2013 17:21:16 +0200 blanchet made theorem extraction code not delve too far when looking at local fact, by relying on 'strip_thm' instead of (wrongly) reverse-engineering proof terms
Fri, 04 Oct 2013 16:11:19 +0200 blanchet more Sledgehammer spying -- record fact indices
Tue, 24 Sep 2013 11:02:42 +0200 blanchet encode goal digest in spying log (to detect duplicates)
Mon, 23 Sep 2013 14:53:43 +0200 blanchet added "spy" option to Sledgehammer
Fri, 12 Jul 2013 20:28:34 +0200 smolkas removed |>! and #>!
Fri, 12 Jul 2013 14:18:07 +0200 smolkas added |>! and #>! for convenient printing of timing information
Tue, 09 Jul 2013 18:45:06 +0200 smolkas completely rewrote SH compress; added two parameters for experimentation/fine grained control
Sat, 11 May 2013 16:57:18 +0200 wenzelm prefer explicitly qualified exceptions, which is particular important for robust handlers;
Mon, 18 Feb 2013 18:34:55 +0100 blanchet implement (more) accurate computation of parents
Thu, 31 Jan 2013 17:54:05 +0100 blanchet tuned data structure
Thu, 31 Jan 2013 17:54:05 +0100 blanchet thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
Fri, 04 Jan 2013 21:56:20 +0100 blanchet refined class handling, to prevent cycles in fact graph
Fri, 04 Jan 2013 21:56:19 +0100 blanchet learn from low-level, inside-class facts
Thu, 20 Dec 2012 15:51:27 +0100 blanchet better weight functions for MePo/MaSh etc.
Sat, 15 Dec 2012 19:57:12 +0100 blanchet thread no timeout properly
Wed, 12 Dec 2012 02:47:45 +0100 blanchet merge aliased theorems in MaSh dependencies, modulo symmetry of equality
Wed, 28 Nov 2012 12:25:43 +0100 smolkas moved thms_of_name to Sledgehammer_Util and removed copies, updated references
Mon, 12 Nov 2012 12:06:56 +0100 blanchet avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit
Mon, 12 Nov 2012 11:52:37 +0100 blanchet centralized term printing code
Fri, 03 Aug 2012 09:51:28 +0200 blanchet cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
Fri, 20 Jul 2012 22:19:46 +0200 blanchet added "learn_from_atp" command to MaSh, for patient users
Fri, 20 Jul 2012 22:19:46 +0200 blanchet learn command in MaSh
Wed, 18 Jul 2012 08:44:04 +0200 blanchet more consolidation of MaSh code
Wed, 18 Jul 2012 08:44:04 +0200 blanchet drastic overhaul of MaSh data structures + fixed a few performance issues
Wed, 18 Jul 2012 08:44:03 +0200 blanchet more code rationalization in relevance filter
Wed, 11 Jul 2012 21:43:19 +0200 blanchet moved most of MaSh exporter code to Sledgehammer
Fri, 16 Mar 2012 11:26:55 +0100 wenzelm clarified Keyword.is_keyword: union of minor and major;
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation
Sun, 29 May 2011 19:40:56 +0200 blanchet normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
Fri, 27 May 2011 10:30:08 +0200 blanchet try both "metis" and (on failure) "metisFT" in replay
Fri, 27 May 2011 10:30:08 +0200 blanchet show time taken for reconstruction
Fri, 27 May 2011 10:30:08 +0200 blanchet use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
Fri, 27 May 2011 10:30:07 +0200 blanchet merge timeout messages from several ATPs into one message to avoid clutter
Fri, 27 May 2011 10:30:07 +0200 blanchet fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
Tue, 24 May 2011 00:01:33 +0200 blanchet eliminated more code duplication in Nitrox
Sun, 22 May 2011 14:51:42 +0200 blanchet improved Waldmeister support -- even run it by default on unit equational goals
Fri, 20 May 2011 12:47:59 +0200 blanchet improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
less more (0) -100 -60 tip