src/HOL/Tools/Nitpick/nitpick_rep.ML
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-03-03 blanchet 2014-03-03 tuned ML names
2014-03-03 blanchet 2014-03-03 tuned code
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
2010-09-13 blanchet 2010-09-13 remove unreferenced identifiers
2010-08-04 blanchet 2010-08-04 get rid of all "optimizations" regarding "unit" and other cardinality-1 types
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
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 added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
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-22 blanchet 2010-02-22 fixed a few bugs in Nitpick and removed unreferenced variables
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"
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-04 blanchet 2009-12-04 fixed paths in Nitpick's ML file headers
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.