2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-09 blanchet 2010-08-09 use "declaration" instead of "setup" to register Nitpick extensions
2010-08-06 blanchet 2010-08-06 local versions of Nitpick.register_xxx functions
2010-08-05 blanchet 2010-08-05 added "whack"
2010-08-05 blanchet 2010-08-05 added support for "Abs_" and "Rep_" functions on quotient types
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 tuning
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-01 blanchet 2010-06-01 remove debug output
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 honor xsymbols in Nitpick
2010-06-01 blanchet 2010-06-01 added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
2010-06-01 blanchet 2010-06-01 thread along context instead of theory for typedef lookup
2010-05-27 blanchet 2010-05-27 Nitpick: show "..." in datatype values (e.g., [{0::nat, ...}]), since these are really equivalence classes
2010-05-01 krauss 2010-05-01 made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
2010-04-25 blanchet 2010-04-25 cosmetics
2010-04-25 blanchet 2010-04-25 remove "show_skolems" option and change style of record declarations
2010-04-25 blanchet 2010-04-25 remove "skolemize" option from Nitpick, since Skolemization is always useful
2010-04-24 blanchet 2010-04-24 removed Nitpick's "uncurry" option
2010-04-24 blanchet 2010-04-24 remove type annotations as comments; Nitpick is now 1136 lines shorter
2010-04-24 blanchet 2010-04-24 cosmetics
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-17 blanchet 2010-03-17 added support for "specification" and "ax_specification" constructs to Nitpick
2010-03-11 blanchet 2010-03-11 moved some Nitpick code around
2010-03-11 blanchet 2010-03-11 added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
2010-03-11 blanchet 2010-03-11 added term postprocessor to Nitpick, to provide custom syntax for typedefs
2010-03-09 blanchet 2010-03-09 added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-27 wenzelm 2010-02-27 clarified @{const_name} vs. @{const_abbrev};
2010-02-26 blanchet 2010-02-26 use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
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-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 improve Nitpick's "Datatypes" rendering for elements containing cycles
2010-02-13 blanchet 2010-02-13 more work on Nitpick's support for nonstandard models + fix in model reconstruction
2010-02-13 blanchet 2010-02-13 redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
2010-02-12 blanchet 2010-02-12 various cosmetic changes to Nitpick
2010-02-10 haftmann 2010-02-10 merged
2010-02-10 haftmann 2010-02-10 moved constants inverse and divide to Ring.thy
2010-02-05 blanchet 2010-02-05 added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
2010-02-05 blanchet 2010-02-05 handle Nitpick's nonstandard model enumeration in a cleaner way; and renumber the atoms so that we get more often a_1 and a_2 and less often a_{n-1} and a_{n-2} in counterexamples
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-04 blanchet 2010-02-04 four changes to Nitpick: 1. avoid writing absolute paths in Kodkodi files for input/output files of external SAT solvers (e.g. MiniSat), to dodge Cygwin problems 2. do eta-contraction in the monotonicity check 3. improved quantifier massaging algorithms using ideas from Paradox 4. repaired "check_potential" and "check_genuine"
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-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
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-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-24 blanchet 2009-11-24 generate clearer atom names in Nitpick for types that end with a digit; requested by a user
2009-11-13 blanchet 2009-11-13 removed a few global names in Nitpick (styp, nat_less, pairf)
2009-11-05 blanchet 2009-11-05 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
2009-10-29 blanchet 2009-10-29 minor cleanup in Nitpick
2009-10-29 blanchet 2009-10-29 fixed error in Nitpick's display of uncurried constants, which resulted in an exception