src/HOL/Nitpick_Examples/Typedef_Nits.thy
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
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 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
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-04-15 blanchet 2013-04-15 not all Nitpick 'constructors' are injective -- careful
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
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-05-11 blanchet 2012-05-11 reintroduced example now that it's no longer broken
2012-05-10 huffman 2012-05-10 temporarily comment out broken nitpick example; adapt to new definition of type rat
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
2012-02-20 huffman 2012-02-20 use qualified constant names instead of suffixes (from Florian Haftmann)
2012-01-03 blanchet 2012-01-03 reintroduced failing examples now that they work again, after reintroduction of "set"
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-09-21 blanchet 2011-09-21 reintroduced Minipick as Nitpick example
2011-08-20 haftmann 2011-08-20 deactivated »unknown« 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.
2011-04-01 krauss 2011-04-01 raised timeouts further, for SML/NJ
2011-03-28 krauss 2011-03-28 raised various timeouts to accommodate sluggish SML/NJ
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-16 huffman 2010-11-16 typedef (open) unit
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-18 haftmann 2010-08-18 adjusted to restored naming convention of logical record types
2010-06-21 blanchet 2010-06-21 compile
2010-06-21 blanchet 2010-06-21 clean up after fcc768dc9dd0
2010-06-11 blanchet 2010-06-11 adjust Nitpick example to follow latest wave of renamings
2010-05-31 blanchet 2010-05-31 obsolete FIXME
2010-02-26 blanchet 2010-02-26 merged
2010-02-26 blanchet 2010-02-26 more work on the new monotonicity stuff in Nitpick
2010-02-24 haftmann 2010-02-24 renamed theory Rational to Rat
2010-02-23 blanchet 2010-02-23 improved precision of small sets 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-04 blanchet 2009-12-04 make proof work again
2009-11-17 blanchet 2009-11-17 fixed "expect" of Nitpick examples to reflect latest changes in Nitpick
2009-10-29 blanchet 2009-10-29 minor cleanup in Nitpick
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.