2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-03-03 blanchet 2014-03-03 fixed handling of 'case_prod' and other 'case' functions for interpreted types
2013-12-06 blanchet 2013-12-06 reverted 86e0b402994c, which was accidentally qfinish'ed and pushed
2013-12-05 blanchet 2013-12-05 experiment
2012-08-15 blanchet 2012-08-15 fixed handling of "int" in the wake of its port to the quotient package
2012-05-30 huffman 2012-05-30 temporarily comment out nitpick examples broken by changes to Int.thy
2012-03-26 blanchet 2012-03-26 fixed Nitpick after numeral representation change (2a1953f0d20d)
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-01-03 blanchet 2012-01-03 tuned import
2011-09-21 blanchet 2011-09-21 reintroduced Minipick as Nitpick example
2011-05-24 blanchet 2011-05-24 use \<emdash> rather than \<midarrow>
2011-04-04 krauss 2011-04-04 raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
2010-12-19 blanchet 2010-12-19 added a timestamp to Nitpick in verbose mode for debugging purposes; turn on verbose mode for the examples
2010-11-03 blanchet 2010-11-03 standardize on seconds for Nitpick and Sledgehammer timeouts
2010-09-14 blanchet 2010-09-14 adapt examples to latest Nitpick changes + speed them up a little bit
2010-08-03 blanchet 2010-08-03 speed up Nitpick examples a little bit
2010-06-21 blanchet 2010-06-21 adjusted Nitpick examples to latest changes + make them slightly faster
2010-03-10 blanchet 2010-03-10 fixed soundness bug in Nitpick
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 added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
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