2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-10-13 haftmann 2011-10-13 bouned transitive closure
2011-08-18 haftmann 2011-08-18 observe distinction between sets and predicates more properly
2011-08-02 krauss 2011-08-02 replaced Nitpick's hardwired basic_ersatz_table by context data
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-03-22 blanchet 2011-03-22 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
2011-02-21 blanchet 2011-02-21 rename Nitpick's (internal) auxiliary lemmas
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
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 fix special handling of set products
2010-09-14 blanchet 2010-09-14 remove more clutter related to old "fast_descrs" optimization
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-08 blanchet 2010-09-08 merge
2010-09-06 blanchet 2010-09-06 remove "minipick" (the toy version of Nitpick) and some tests; a small step towards making the Nitpick tests take less time
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-12 haftmann 2010-08-12 group record-related ML files
2010-07-03 blanchet 2010-07-03 adapt Nitpick to "prod_case" and "*" -> "sum" renaming; the code in "Nitpick_Preproc", which sorted the types using "typ_ord", was wrong and evil; it seems to have worked only because "*" was called "*"
2010-06-11 blanchet 2010-06-11 adjust Nitpick's handling of "<" on "rat"s and "reals"
2010-05-31 blanchet 2010-05-31 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
2010-05-14 blanchet 2010-05-14 add "no_atp"s to Nitpick lemmas
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-17 blanchet 2010-03-17 added support for "specification" and "ax_specification" constructs to Nitpick
2010-03-10 blanchet 2010-03-10 improve precision of "card" in Nitpick
2010-03-09 blanchet 2010-03-09 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
2010-03-09 blanchet 2010-03-09 added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
2010-02-23 blanchet 2010-02-23 improved Nitpick's support for quotient types
2010-02-22 blanchet 2010-02-22 enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
2010-02-18 blanchet 2010-02-18 added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
2010-02-13 blanchet 2010-02-13 more work on Nitpick's support for nonstandard models + fix in model reconstruction
2010-02-12 blanchet 2010-02-12 various cosmetic changes to Nitpick
2010-02-09 blanchet 2010-02-09 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
2010-02-04 blanchet 2010-02-04 split "nitpick_hol.ML" into two files to make it more manageable; more refactoring to come
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-02-02 blanchet 2010-02-02 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2010-01-20 blanchet 2010-01-20 fix issues with previous Nitpick change
2009-12-17 blanchet 2009-12-17 added support for binary nat/int representation to Nitpick
2009-11-17 blanchet 2009-11-17 bump up Nitpick's axiom/definition unfolding limits, because some real-world problems (e.g. from Boogie) ran into the previous limits; the limits are there to prevent infinite recursion; they can be set arbitrarily high without much harm
2009-11-11 haftmann 2009-11-11 tuned imports
2009-10-28 blanchet 2009-10-28 merged my Auto Nitpick change with Lukas's Predicate Compiler changes
2009-10-28 blanchet 2009-10-28 introduced Auto Nitpick in addition to Auto Quickcheck; this required generalizing the theorem hook used by Quickcheck, following a suggestion by Florian
2009-10-27 blanchet 2009-10-27 renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
2009-10-27 haftmann 2009-10-27 dropped obsolete comment
2009-10-22 blanchet 2009-10-22 added Nitpick's theory and ML files to Isabelle/HOL; the examples and the documentation are on their way.