src/HOL/Tools/Nitpick/nitpick_kodkod.ML
Thu, 01 Mar 2012 11:28:56 +0100 blanchet more robust set element extractor
Tue, 03 Jan 2012 18:33:18 +0100 blanchet handle "Id" gracefully w.r.t. "set"
Tue, 03 Jan 2012 18:33:18 +0100 blanchet rationalized output (a bit)
Tue, 03 Jan 2012 18:33:17 +0100 blanchet fixed a few more bugs in \Nitpick's new "set" support
Tue, 03 Jan 2012 18:33:17 +0100 blanchet port part of Nitpick to "set" type constructor
Wed, 20 Apr 2011 16:49:21 +0200 blanchet worked around Kodkodi limitation with parsing {}, where it cannot easily deduce its arity -- without this workaround, Kodkod sometimes generates arity errors in conjunction with the "need" option since change 614ff13dc5d2
Sat, 19 Mar 2011 14:03:13 +0100 blanchet preencode value of "need" selectors in Kodkod bounds as an optimization
Sat, 19 Mar 2011 11:22:23 +0100 blanchet ignore "need" axioms for "nat"-like types
Fri, 18 Mar 2011 17:27:28 +0100 blanchet optimize Kodkod axioms further w.r.t. "need" option
Fri, 18 Mar 2011 12:20:32 +0100 blanchet optimize Kodkod bounds of nat-like datatypes
Fri, 18 Mar 2011 12:05:23 +0100 blanchet more optimizations of bounds for "need"
Fri, 18 Mar 2011 11:43:28 +0100 blanchet optimize Kodkod bounds when "need" is specified
Tue, 15 Mar 2011 15:49:42 +0100 blanchet support non-ground "need" values
Thu, 03 Mar 2011 11:20:48 +0100 blanchet renamed "preconstr" option "need"
Mon, 21 Feb 2011 17:36:32 +0100 blanchet more work on "fix_datatype_vals" optimization (renamed "preconstruct")
Mon, 21 Feb 2011 16:33:21 +0100 blanchet more work on "fix_datatype_vals"
Mon, 21 Feb 2011 15:45:44 +0100 blanchet first steps in implementing "fix_datatype_vals" optimization
Tue, 07 Dec 2010 11:56:01 +0100 blanchet removed needless optimization for image -- there might be cases that benefit from it but there are others where it is clearly evil
Tue, 07 Dec 2010 11:56:01 +0100 blanchet simplified special handling of set products
Tue, 07 Dec 2010 11:56:01 +0100 blanchet use heuristic to determine whether to keep or drop an existing "let" -- and drop all higher-order lets
Fri, 01 Oct 2010 10:58:01 +0200 blanchet tuning
Thu, 16 Sep 2010 14:24:03 +0200 blanchet tuning
Tue, 14 Sep 2010 13:44:43 +0200 blanchet eliminate more clutter related to "fast_descrs" optimization
Tue, 14 Sep 2010 12:52:50 +0200 blanchet fixed bug in the "fast_descrs" optimization;
Mon, 13 Sep 2010 20:21:40 +0200 blanchet remove unreferenced identifiers
Sat, 11 Sep 2010 10:20:25 +0200 blanchet change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
Fri, 06 Aug 2010 10:50:52 +0200 blanchet improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
Thu, 05 Aug 2010 01:12:12 +0200 blanchet remove buggy and needless condition
Thu, 05 Aug 2010 00:21:11 +0200 blanchet renamed internal function
Wed, 04 Aug 2010 23:27:27 +0200 blanchet Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
less more (0) -50 -30 tip