src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
Fri, 05 Mar 2021 16:09:42 +0100 wenzelm clarified signature --- augment existing structure Time;
Thu, 29 Oct 2020 16:07:41 +0100 desharna Added smt (verit) to Sledgehammer's proof preplay.
Fri, 11 Oct 2019 15:36:32 +0200 wenzelm clarified signature;
Wed, 24 Jan 2018 18:54:05 +0100 wenzelm tuned: prefer list operations over Source.source;
Tue, 06 Jun 2017 13:13:25 +0200 wenzelm discontinued obsolete print mode;
Fri, 16 Dec 2016 14:06:31 +0100 wenzelm tuned signature -- more abstract type thm_node;
Thu, 22 Sep 2016 11:25:27 +0200 wenzelm discontinued raw symbols;
Sun, 14 Aug 2016 12:26:09 +0200 blanchet killed final stops in Sledgehammer and friends
Wed, 13 Apr 2016 18:01:05 +0200 wenzelm eliminated "xname" and variants;
Sat, 02 Apr 2016 23:29:05 +0200 wenzelm prefer infix operations;
Thu, 15 Oct 2015 12:39:51 +0200 blanchet removed too aggressive underscorization
Mon, 05 Oct 2015 23:03:50 +0200 blanchet further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Sat, 24 Jan 2015 22:00:24 +0100 wenzelm tuned signature;
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
less more (0) -100 -60 tip