src/HOL/Tools/Nitpick/nitpick_hol.ML
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
2009-10-27 blanchet 2009-10-27 clean Nitpick's wellfoundedness cache once in a while, to avoid potential memory leak
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-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-30 krauss 2009-10-30 less verbose termination tactics
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-26 blanchet 2009-10-26 make Nitpick compile again
2009-10-23 blanchet 2009-10-23 be somewhat more liberal in Nitpick about which types may occur in formulas
2009-10-23 blanchet 2009-10-23 continuation of Nitpick's integration into Isabelle; added examples, and integrated non-Main theories better.
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.