src/HOL/Nitpick_Examples/Refute_Nits.thy
2010-04-23 wenzelm 2010-04-23 mark schematic statements explicitly;
2010-03-01 wenzelm 2010-03-01 repaired 'definition' (cf. d8d7d1b785af);
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-24 blanchet 2010-02-24 compile
2010-02-24 blanchet 2010-02-24 compile
2010-02-24 blanchet 2010-02-24 got rid of "axclass", apparently
2010-02-22 blanchet 2010-02-22 enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
2010-02-10 blanchet 2010-02-10 make Nitpick test a bit weaker; this should solve failure observed last night on "mac-poly"
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-14 blanchet 2009-12-14 make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits
2009-11-17 blanchet 2009-11-17 use SAT solver that's available everywhere for this example
2009-10-23 blanchet 2009-10-23 continuation of Nitpick's integration into Isabelle; added examples, and integrated non-Main theories better.