src/HOL/Tools/Nitpick/nitpick_hol.ML
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.