src/HOL/Nitpick_Examples/Mini_Nits.thy
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2013-12-21 blanchet 2013-12-21 compile + reduce problem size by a notch
2013-12-06 blanchet 2013-12-06 reverted 86e0b402994c, which was accidentally qfinish'ed and pushed
2013-12-05 blanchet 2013-12-05 experiment
2013-02-25 wenzelm 2013-02-25 prefer stateless 'ML_val' for tests;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-09-23 blanchet 2011-09-23 first step towards extending Minipick with more translations
2011-09-21 blanchet 2011-09-21 reintroduced Minipick as Nitpick example
2010-06-22 blanchet 2010-06-22 make the Nitpick_Example theory processable even when Kodkodi is not installed; so that at least the "theory" aspects of it (as opposed to the diagnosis offered by Nitpick) are checked on everybody's machines
2010-03-10 blanchet 2010-03-10 improve precision of "card" in Nitpick
2010-02-22 blanchet 2010-02-22 enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
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-10-23 blanchet 2009-10-23 continuation of Nitpick's integration into Isabelle; added examples, and integrated non-Main theories better.