src/HOL/Nitpick_Examples/Nitpick_Examples.thy
2011-09-21 blanchet 2011-09-21 reintroduced Minipick as Nitpick example
2010-09-06 blanchet 2010-09-06 remove "minipick" (the toy version of Nitpick) and some tests; a small step towards making the Nitpick tests take less time
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
2009-10-23 blanchet 2009-10-23 continuation of Nitpick's integration into Isabelle; added examples, and integrated non-Main theories better.