src/HOL/Nitpick_Examples/Refute_Nits.thy
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 ported Nitpick_Examples to new datatypes
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
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-03-03 blanchet 2014-03-03 rationalized internals
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'
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2014-02-12 blanchet 2014-02-12 adapted theories to '{case,rec}_{list,option}' names
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-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
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-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-08-03 blanchet 2010-08-03 speed up Nitpick examples a little bit
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.