src/HOL/Tools/Nitpick/nitpick_util.ML
2010-08-23 ago perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
2010-08-06 ago local versions of Nitpick.register_xxx functions
2010-08-05 ago fiddle with specialization etc.
2010-08-05 ago fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
2010-08-03 ago better "Pretty" handling
2010-07-27 ago remove unused fun
2010-06-01 ago honor xsymbols in Nitpick
2010-06-01 ago added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
2010-04-29 ago expand combinators in Isar proofs constructed by Sledgehammer;
2010-04-27 ago remove Nitpick functions that are now implemented in Sledgehammer
2010-04-24 ago remove type annotations as comments;
2010-04-23 ago stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
2010-03-23 ago leverage code now in Sledgehammer
2010-03-19 ago move the Sledgehammer Isar commands together into one file;
2010-03-17 ago added support for "specification" and "ax_specification" constructs to Nitpick
2010-02-25 ago improved precision of infinite "shallow" datatypes in Nitpick;
2010-02-22 ago fixed a few bugs in Nitpick and removed unreferenced variables
2010-02-18 ago added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
2010-02-02 ago added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2010-01-20 ago some work on Nitpick's support for quotient types;
2009-12-17 ago added support for binary nat/int representation to Nitpick
2009-12-08 ago made Nitpick work also for people who import "Plain" instead of "Main"
2009-12-04 ago fixed paths in Nitpick's ML file headers
2009-11-13 ago removed a few global names in Nitpick (styp, nat_less, pairf)
2009-10-27 ago internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
2009-10-22 ago added Nitpick's theory and ML files to Isabelle/HOL;