src/HOL/Tools/Nitpick/nitpick_scope.ML
2010-12-07 blanchet 2010-12-07 remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
2010-09-03 wenzelm 2010-09-03 turned show_all_types into proper configuration option;
2010-08-06 blanchet 2010-08-06 local versions of Nitpick.register_xxx functions
2010-08-04 blanchet 2010-08-04 improve datatype symmetry breaking; all based on "datatype bin_list = BNil | B0Cons bin_list | B1Cons bin_list" example
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 better "Pretty" handling
2010-08-03 blanchet 2010-08-03 change formula for enumerating scopes
2010-08-03 blanchet 2010-08-03 example tweaking -- also prevents Nitpick_Tests from using more than 1 thread
2010-08-03 blanchet 2010-08-03 bump up the max cardinalities, to use up more of the time given to us by the user
2010-08-02 blanchet 2010-08-02 minor symmetry breaking for codatatypes like llist
2010-08-01 blanchet 2010-08-01 tweak datatype sym break code
2010-08-01 blanchet 2010-08-01 added manual symmetry breaking for datatypes
2010-07-31 blanchet 2010-07-31 started implementation of custom sym break
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-01 blanchet 2010-06-01 thread along context instead of theory for typedef lookup
2010-04-25 blanchet 2010-04-25 remove "show_skolems" option and change style of record declarations
2010-04-24 blanchet 2010-04-24 Fruhjahrsputz: remove three mostly useless Nitpick options
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-04-23 blanchet 2010-04-23 stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
2010-03-24 blanchet 2010-03-24 simplify Nitpick parameter parsing code a little bit + make compile
2010-03-17 blanchet 2010-03-17 added one-entry cache around Kodkod invocation
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-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-13 blanchet 2010-02-13 redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)
2010-02-12 blanchet 2010-02-12 minor fixes to Nitpick
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-05 blanchet 2010-02-05 optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil"; this gains one cardinality in the AA tree examples in the Nitpick manual
2010-02-04 blanchet 2010-02-04 adapted example following previous Nitpick change and fixed minor optimization in Nitpick
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-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 fixed paths in Nitpick's ML file headers
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-23 blanchet 2009-11-23 fixed soundness bug in Nitpick that occurred because unrolled predicate iterators were considered to be a "precise" type
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-27 blanchet 2009-10-27 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
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.