src/HOL/Nitpick_Examples/Manual_Nits.thy
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-10-10 wenzelm 2012-10-10 eliminated some remaining uses of typedef with implicit set definition;
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 fixed "real" after they were redefined as a 'quotient_type'
2012-05-10 huffman 2012-05-10 temporarily comment out broken nitpick example
2012-03-23 kuncar 2012-03-23 fix Quotient_Examples
2012-01-09 blanchet 2012-01-09 revert unintended "sledgehammer" call
2012-01-03 blanchet 2012-01-03 tuning
2012-01-03 blanchet 2012-01-03 updated Nitpick docs after "set" reintroduction
2012-01-03 blanchet 2012-01-03 no abuse of notation
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-23 blanchet 2011-09-23 synchronized section names with manual
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-20 blanchet 2011-04-20 increase "auto"'s timeout in example to help SML/NJ
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-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
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 adapt examples to latest Nitpick changes + speed them up a little bit
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-09 blanchet 2010-08-09 "declare" -> "declaration" (typo)
2010-08-09 blanchet 2010-08-09 use "declaration" instead of "setup" to register Nitpick extensions
2010-08-06 blanchet 2010-08-06 adapt occurrences of renamed Nitpick functions
2010-08-03 blanchet 2010-08-03 minor changes
2010-06-21 blanchet 2010-06-21 adjusted Nitpick examples to latest changes + make them slightly faster
2010-04-21 blanchet 2010-04-21 use only one thread in "Manual_Nits"; the second thread isn't helping much, and might very well be the cause of the Cygwin Isatest failure
2010-03-12 blanchet 2010-03-12 make tests less demanding, to prevent sporadic failures
2010-03-11 blanchet 2010-03-11 moved some Nitpick code around
2010-03-11 blanchet 2010-03-11 added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
2010-03-11 blanchet 2010-03-11 added term postprocessor to Nitpick, to provide custom syntax for typedefs
2010-03-11 blanchet 2010-03-11 made "Manual_Nits" tests more robust
2010-03-09 blanchet 2010-03-09 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
2010-03-09 blanchet 2010-03-09 added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
2010-02-23 blanchet 2010-02-23 improved precision of small sets in Nitpick
2010-02-23 blanchet 2010-02-23 catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
2010-02-22 blanchet 2010-02-22 enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
2010-02-17 blanchet 2010-02-17 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
2010-02-13 blanchet 2010-02-13 more work on Nitpick's support for nonstandard models + fix in model reconstruction
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
2010-02-02 blanchet 2010-02-02 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
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.