2011-05-05 blanchet 2011-05-05 query typedefs as well for monotonicity
2011-05-04 blanchet 2011-05-04 exploit inferred monotonicity
2011-05-04 blanchet 2011-05-04 [mq]: nitpick_tuning
2011-05-04 blanchet 2011-05-04 fixed cardinality computation for function types such as "'a -> unit"
2011-04-20 wenzelm 2011-04-20 added Theory.nodes_of convenience;
2011-04-19 blanchet 2011-04-19 avoid relying on "Thm.definitionK" to pick up definitions -- this was an old hack related to locales (to avoid expanding locale constants to their low-level definition) that is no longer necessary
2011-04-19 blanchet 2011-04-19 use "Spec_Rules" for finding axioms -- more reliable and cleaner
2011-04-19 blanchet 2011-04-19 optimize trivial equalities early in Nitpick -- it shouldn't be the job of the peephole optimizer
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-18 blanchet 2011-03-18 always destroy constructor patterns, since this seems to be always useful
2011-03-09 blanchet 2011-03-09 improved formula for specialization, to prevent needless specializations -- and removed dead code
2011-03-03 blanchet 2011-03-03 simplify "need" option's syntax
2011-03-03 blanchet 2011-03-03 renamed "preconstr" option "need"
2011-03-02 blanchet 2011-03-02 lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
2011-02-28 blanchet 2011-02-28 improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)
2011-02-28 blanchet 2011-02-28 made "fixed_is_special_eligible_arg" smarter w.r.t. pairs, and fixed previous unintended behavior because "andalso" ties more tightly than "orelse"
2011-02-21 blanchet 2011-02-21 more work on "fix_datatype_vals" optimization (renamed "preconstruct")
2011-02-21 blanchet 2011-02-21 improve optimization
2011-02-21 blanchet 2011-02-21 tweaked Nitpick based on C++ memory model example
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2011-02-21 blanchet 2011-02-21 always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-12-07 blanchet 2010-12-07 remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
2010-12-07 blanchet 2010-12-07 removed needless optimization for image -- there might be cases that benefit from it but there are others where it is clearly evil
2010-12-07 blanchet 2010-12-07 simplified special handling of set products
2010-12-07 blanchet 2010-12-07 fix special handling of set products
2010-12-07 blanchet 2010-12-07 use heuristic to determine whether to keep or drop an existing "let" -- and drop all higher-order lets
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-09-24 wenzelm 2010-09-24 modernized structure Ord_List;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-14 blanchet 2010-09-14 eliminate more clutter related to "fast_descrs" optimization
2010-09-14 blanchet 2010-09-14 remove "fast_descs" option from Nitpick; the option has been unsound for over a year and is too imprecise to be of any use when made sound
2010-09-13 blanchet 2010-09-13 remove unreferenced identifiers
2010-09-11 blanchet 2010-09-11 always handle type variables in typedefs as global
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-23 blanchet 2010-08-23 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later; it's a mistake to transform the elim rules too early because then we lose some info, e.g. "no_atp" attributes
2010-08-09 blanchet 2010-08-09 use "declaration" instead of "setup" to register Nitpick extensions
2010-08-09 blanchet 2010-08-09 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
2010-08-06 blanchet 2010-08-06 added support for partial quotient types; previously Nitpick was unsound for these
2010-08-06 blanchet 2010-08-06 adapt occurrences of renamed Nitpick functions
2010-08-06 blanchet 2010-08-06 local versions of Nitpick.register_xxx functions
2010-08-06 blanchet 2010-08-06 quotient types registered as codatatypes are no longer quotient types
2010-08-06 blanchet 2010-08-06 improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
2010-08-05 blanchet 2010-08-05 added "whack"
2010-08-05 blanchet 2010-08-05 handle "Rep_unit" & Co. gracefully
2010-08-05 blanchet 2010-08-05 added support for "Abs_" and "Rep_" functions on quotient types
2010-08-05 blanchet 2010-08-05 fiddle with specialization etc.
2010-08-05 blanchet 2010-08-05 handle inductive predicates correctly after change in "def" semantics
2010-08-05 blanchet 2010-08-05 don't specialize built-ins or constructors
2010-08-05 blanchet 2010-08-05 prevent the expansion of too large definitions -- use equations for these instead
2010-08-05 blanchet 2010-08-05 make nitpick accept "==" for "nitpick_(p)simp"s
2010-08-05 blanchet 2010-08-05 fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
2010-08-04 blanchet 2010-08-04 get rid of all "optimizations" regarding "unit" and other cardinality-1 types
2010-08-03 blanchet 2010-08-03 better "Pretty" handling
2010-08-03 blanchet 2010-08-03 bump up the max cardinalities, to use up more of the time given to us by the user
2010-08-03 blanchet 2010-08-03 fix newly introduced bug w.r.t. conditional equations
2010-08-03 blanchet 2010-08-03 make Nitpick more flexible when parsing (p)simp rules
2010-08-03 blanchet 2010-08-03 optimize local "def"s by treating them as definitions