src/HOL/Tools/Nitpick/nitpick_hol.ML
Thu, 03 Mar 2011 11:20:48 +0100 blanchet simplify "need" option's syntax
Thu, 03 Mar 2011 11:20:48 +0100 blanchet renamed "preconstr" option "need"
Wed, 02 Mar 2011 14:50:16 +0100 blanchet lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
Mon, 28 Feb 2011 17:53:10 +0100 blanchet improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
Mon, 28 Feb 2011 17:53:10 +0100 blanchet made "fixed_is_special_eligible_arg" smarter w.r.t. pairs, and fixed previous unintended behavior because "andalso" ties more tightly than "orelse"
Mon, 21 Feb 2011 17:36:32 +0100 blanchet more work on "fix_datatype_vals" optimization (renamed "preconstruct")
Mon, 21 Feb 2011 11:50:38 +0100 blanchet improve optimization
Mon, 21 Feb 2011 11:50:31 +0100 blanchet tweaked Nitpick based on C++ memory model example
Mon, 21 Feb 2011 10:44:19 +0100 blanchet renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
Mon, 21 Feb 2011 10:42:29 +0100 blanchet always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
Sat, 08 Jan 2011 17:14:48 +0100 wenzelm misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
Tue, 07 Dec 2010 11:56:53 +0100 blanchet remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
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 fix 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
Mon, 25 Oct 2010 21:06:56 +0200 wenzelm renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
Fri, 24 Sep 2010 15:53:13 +0200 wenzelm modernized structure Ord_List;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Tue, 14 Sep 2010 13:44:43 +0200 blanchet eliminate more clutter related to "fast_descrs" optimization
Tue, 14 Sep 2010 13:24:18 +0200 blanchet remove "fast_descs" option from Nitpick;
Mon, 13 Sep 2010 20:21:40 +0200 blanchet remove unreferenced identifiers
Sat, 11 Sep 2010 10:13:51 +0200 blanchet always handle type variables in typedefs as global
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Fri, 27 Aug 2010 10:56:46 +0200 haftmann formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
Thu, 26 Aug 2010 20:51:17 +0200 haftmann formerly unnamed infix impliciation now named HOL.implies
Mon, 23 Aug 2010 14:54:17 +0200 blanchet perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
Mon, 09 Aug 2010 12:40:15 +0200 blanchet use "declaration" instead of "setup" to register Nitpick extensions
Mon, 09 Aug 2010 12:05:48 +0200 blanchet move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
Fri, 06 Aug 2010 18:11:30 +0200 blanchet added support for partial quotient types;
Fri, 06 Aug 2010 17:23:11 +0200 blanchet adapt occurrences of renamed Nitpick functions
Fri, 06 Aug 2010 17:05:29 +0200 blanchet local versions of Nitpick.register_xxx functions
Fri, 06 Aug 2010 11:35:10 +0200 blanchet quotient types registered as codatatypes are no longer quotient types
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 20:17:50 +0200 blanchet added "whack"
Thu, 05 Aug 2010 18:33:07 +0200 blanchet handle "Rep_unit" & Co. gracefully
Thu, 05 Aug 2010 18:00:50 +0200 blanchet added support for "Abs_" and "Rep_" functions on quotient types
Thu, 05 Aug 2010 15:44:54 +0200 blanchet fiddle with specialization etc.
Thu, 05 Aug 2010 14:45:27 +0200 blanchet handle inductive predicates correctly after change in "def" semantics
Thu, 05 Aug 2010 14:32:24 +0200 blanchet don't specialize built-ins or constructors
Thu, 05 Aug 2010 14:10:18 +0200 blanchet prevent the expansion of too large definitions -- use equations for these instead
Thu, 05 Aug 2010 12:58:57 +0200 blanchet make nitpick accept "==" for "nitpick_(p)simp"s
Thu, 05 Aug 2010 12:40:12 +0200 blanchet fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
Wed, 04 Aug 2010 10:39:35 +0200 blanchet get rid of all "optimizations" regarding "unit" and other cardinality-1 types
Tue, 03 Aug 2010 21:20:31 +0200 blanchet better "Pretty" handling
Tue, 03 Aug 2010 14:49:42 +0200 blanchet bump up the max cardinalities, to use up more of the time given to us by the user
Tue, 03 Aug 2010 13:29:26 +0200 blanchet fix newly introduced bug w.r.t. conditional equations
Tue, 03 Aug 2010 12:31:30 +0200 blanchet make Nitpick more flexible when parsing (p)simp rules
Tue, 03 Aug 2010 01:16:08 +0200 blanchet optimize local "def"s by treating them as definitions
Mon, 02 Aug 2010 19:15:15 +0200 blanchet careful about which linear inductive predicates should be starred
Mon, 02 Aug 2010 14:27:20 +0200 blanchet prefer implication to equality, to be more SAT solver friendly
Mon, 02 Aug 2010 12:36:50 +0200 blanchet fix bug with mutually recursive and nested codatatypes
Thu, 01 Jul 2010 16:54:44 +0200 haftmann "prod" and "sum" replace "*" and "+" respectively
Mon, 28 Jun 2010 15:03:07 +0200 haftmann merged constants "split" and "prod_case"
Mon, 21 Jun 2010 14:07:00 +0200 blanchet sort cases on the proper key
Mon, 21 Jun 2010 11:15:21 +0200 blanchet optimized code generated for datatype cases + more;
Tue, 01 Jun 2010 17:28:16 +0200 blanchet cosmetics
Tue, 01 Jun 2010 15:38:47 +0200 blanchet removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
Tue, 01 Jun 2010 14:14:02 +0200 blanchet honor xsymbols in Nitpick
Tue, 01 Jun 2010 12:20:08 +0200 blanchet added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
less more (0) -100 -60 tip