src/HOL/Nitpick_Examples/Core_Nits.thy
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-03 blanchet 2014-03-03 fixed handling of 'case_prod' and other 'case' functions for interpreted types
2014-02-12 blanchet 2014-02-12 removed trivial 'rec' examples for nonrecursive types (I could also have added the 'old.' prefix in front of the constant names)
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-01-03 blanchet 2012-01-03 fixed type annotations
2012-01-03 blanchet 2012-01-03 fixed a few more bugs in \Nitpick's new "set" support
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
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-19 blanchet 2011-04-19 remove a few Nitpick calls in examples -- another step toward making them run faster
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 remove "fast_descs" option from Nitpick; the option has been unsound for over a year and is too imprecise to be of any use when made sound
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-08-03 blanchet 2010-08-03 speed up Nitpick examples a little bit
2010-07-03 blanchet 2010-07-03 adapt Nitpick to "prod_case" and "*" -> "sum" renaming; the code in "Nitpick_Preproc", which sorted the types using "typ_ord", was wrong and evil; it seems to have worked only because "*" was called "*"
2010-06-28 haftmann 2010-06-28 merged constants "split" and "prod_case" -- nitpick behaves differently
2010-06-15 blanchet 2010-06-15 make example run a bit faster (might help atbroy102)
2010-06-02 blanchet 2010-06-02 fix parameter settings
2010-06-01 blanchet 2010-06-01 added examples/tests for THE and SOME
2010-05-28 blanchet 2010-05-28 remove two examples, now that the definition of "fst" and "snd" has changed
2010-04-23 wenzelm 2010-04-23 mark schematic statements explicitly;
2010-02-26 blanchet 2010-02-26 more work on the new monotonicity stuff in Nitpick
2010-02-22 blanchet 2010-02-22 enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
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
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-12-14 blanchet 2009-12-14 make Nitpick "Core" test more conservative, to avoid problems on Larry's machine
2009-10-23 blanchet 2009-10-23 make the Nitpick examples work again
2009-10-23 blanchet 2009-10-23 continuation of Nitpick's integration into Isabelle; added examples, and integrated non-Main theories better.