src/HOL/Tools/Nitpick/nitpick_hol.ML
2010-03-29 blanchet 2010-03-29 get rid of Polyhash, since it's no longer used
2010-03-27 wenzelm 2010-03-27 Typedef.info: separate global and local part, only the latter is transformed by morphisms;
2010-03-22 blanchet 2010-03-22 detect OFCLASS() axioms in Nitpick; this is necessary now that "Thy.all_axioms_of" returns such axiom (starting with change 46cfc4b8112e)
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-13 wenzelm 2010-03-13 adapted to localized typedef: handle single global interpretation only;
2010-03-11 blanchet 2010-03-11 moved some Nitpick code around
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 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-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
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-26 blanchet 2010-02-26 more work on the new monotonicity stuff in Nitpick
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-25 blanchet 2010-02-25 cosmetics
2010-02-23 blanchet 2010-02-23 support local definitions in Nitpick
2010-02-23 blanchet 2010-02-23 optimized multisets in Nitpick by fishing "finite"
2010-02-23 blanchet 2010-02-23 improved Nitpick's support for quotient types
2010-02-23 blanchet 2010-02-23 catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
2010-02-22 blanchet 2010-02-22 enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
2010-02-22 blanchet 2010-02-22 filter out trivial definitions in Nitpick (e.g. "Topology.topo" from AFP)
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 synchronize Nitpick's wellfoundedness formulas caching
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-09 blanchet 2010-02-09 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
2010-02-09 blanchet 2010-02-09 optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
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-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
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-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 fix soundness bug in Nitpick's "destroy_constrs" optimization
2009-11-30 haftmann 2009-11-30 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-24 blanchet 2009-11-24 fix soundness bug in "uncurry" option of Nitpick
2009-11-24 blanchet 2009-11-24 fix soundness bug in Nitpick's handling of negative literals (e.g., -1::rat)
2009-11-24 blanchet 2009-11-24 fixed soundness bug / type error in handling of unpolarized (co)inductive predicates in Nitpick
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's handling of typedefs
2009-11-23 blanchet 2009-11-23 fix Nitpick soundness bugs related to integration (in particular, "code_numeral")
2009-11-23 blanchet 2009-11-23 fixed error in Nitpick's "star_linear_preds" optimization, which resulted in an ill-typed term; reported by Stefan
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-17 blanchet 2009-11-17 made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
2009-11-16 blanchet 2009-11-16 merged
2009-11-13 blanchet 2009-11-13 removed a few global names in Nitpick (styp, nat_less, pairf)
2009-11-15 wenzelm 2009-11-15 primitive defs: clarified def (axiom name) vs. description;
2009-11-15 wenzelm 2009-11-15 permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);
2009-11-10 blanchet 2009-11-10 merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
2009-11-05 blanchet 2009-11-05 added possibility to register datatypes as codatatypes in Nitpick; this is useful if the datatype is used only as a means to define the codatatype
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-11-05 blanchet 2009-11-05 merged
2009-10-29 blanchet 2009-10-29 minor cleanup in Nitpick