src/HOL/Tools/Nitpick/nitpick_nut.ML
2012-04-03 griff 2012-04-03 renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
2012-01-04 blanchet 2012-01-04 improved "set" support by code inspection
2012-01-03 blanchet 2012-01-03 rationalized output (a bit)
2012-01-03 blanchet 2012-01-03 fixed a few more bugs in \Nitpick's new "set" support
2012-01-03 blanchet 2012-01-03 port part of Nitpick to "set" type constructor
2011-04-19 blanchet 2011-04-19 check arity of bound variables to avoid generating too large Kodkod problems -- an issue that arose in the context of TPTP/CASC
2011-02-28 blanchet 2011-02-28 added "total_consts" option
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-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 move equation up where it's not ignored
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-04 blanchet 2010-08-04 get rid of all "optimizations" regarding "unit" and other cardinality-1 types
2010-08-03 blanchet 2010-08-03 fix soundness bug w.r.t. "Suc" with "binary_ints"
2010-08-03 blanchet 2010-08-03 handle free variables even more gracefully; 1. show those that only occur in assumptions as part of the constants; 2. make sure locally defined Frees are given an Opt rep, just like constants generally owuld
2010-08-01 blanchet 2010-08-01 added manual symmetry breaking for datatypes
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-21 blanchet 2010-06-21 make Nitpick's unsound mode a bit more unsound
2010-06-21 blanchet 2010-06-21 optimized code generated for datatype cases + more; more = lazy creation of debugging messages in mono code + use of "let" when performing some beta-applications (to avoid exponential blowup) + removal of some set constructs, to simplify the code and increase precision in some cases (and decrease it in others, but this can be regained)
2010-06-01 blanchet 2010-06-01 improved precision of "set" based on an example from Lukas
2010-06-01 blanchet 2010-06-01 don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
2010-06-01 blanchet 2010-06-01 thread along context instead of theory for typedef lookup
2010-05-14 blanchet 2010-05-14 improve precision of set constructs in Nitpick
2010-05-14 blanchet 2010-05-14 produce more potential counterexamples for subset operator (cf. quantifiers)
2010-04-24 blanchet 2010-04-24 remove type annotations as comments; Nitpick is now 1136 lines shorter
2010-04-13 blanchet 2010-04-13 make Nitpick output everything to tracing in debug mode; so that when an exception occurs, I can switch to the tracing window to see what was in the response window before the exception blew everything away
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-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-25 blanchet 2010-02-25 improved precision of infinite "shallow" datatypes in Nitpick; e.g. strings used for variable names, instead of an opaque type
2010-02-23 blanchet 2010-02-23 improved precision of small sets in Nitpick
2010-02-22 blanchet 2010-02-22 fixed a few bugs in Nitpick and removed unreferenced variables
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-17 blanchet 2010-02-17 make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
2010-02-17 blanchet 2010-02-17 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
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 some work on Nitpick's support for quotient types; quotient types are not yet in Isabelle, so for now I hardcoded "IntEx.my_int"
2010-01-07 blanchet 2010-01-07 reduced arity of Nitpick selectors associated with sets by 1, by using "Formula" instead of "Atom 2"
2009-12-18 blanchet 2009-12-18 polished Nitpick's binary integer support etc.; etc. = improve inconsistent scope correction + sort values nicely in output + handle "mod" using the characterization "x mod y = x - x div y * y" (instead of explicit code in Nitpick) + introduce KK = Kodkod as abbreviation
2009-12-17 blanchet 2009-12-17 added support for binary nat/int representation to Nitpick
2009-12-14 blanchet 2009-12-14 distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick; this improves Nitpick's precision in some cases (e.g. higher-order constructors) and reflects a better understanding of what's going on
2009-12-14 blanchet 2009-12-14 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
2009-12-04 blanchet 2009-12-04 fixed paths in Nitpick's ML file headers
2009-11-23 blanchet 2009-11-23 fix Nitpick soundness bug related to "finite (UNIV::'a set)" where "'a" is constrained by a sort to be infinite
2009-11-23 blanchet 2009-11-23 fixed soundness bug in Nitpick that occurred because unrolled predicate iterators were considered to be a "precise" type
2009-11-17 blanchet 2009-11-17 fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
2009-11-12 blanchet 2009-11-12 fixed soundness bug in Nitpick related to sets
2009-10-29 blanchet 2009-10-29 minor cleanup in Nitpick
2009-10-27 blanchet 2009-10-27 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
2009-10-27 blanchet 2009-10-27 internal renaming in Nitpick and fixed Kodkodi invokation on Linux; renamed Nitpick's ML structures from NitpickXxx to Nitpick_Xxx and added KODKODI_JAVA_LIBRARY_PATH to LD_LIBRARY_PATH before invoking Kodkodi
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.