src/HOL/Nitpick_Examples/Refute_Nits.thy
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Wed, 21 Sep 2011 15:55:16 +0200 blanchet reintroduced Minipick as Nitpick example
Tue, 24 May 2011 00:01:33 +0200 blanchet use \<emdash> rather than \<midarrow>
Tue, 19 Apr 2011 12:21:57 +0200 blanchet remove a few Nitpick calls in examples -- another step toward making them run faster
Mon, 04 Apr 2011 09:32:50 +0200 krauss raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
Sun, 19 Dec 2010 11:48:42 +0100 blanchet added a timestamp to Nitpick in verbose mode for debugging purposes;
Wed, 03 Nov 2010 22:26:53 +0100 blanchet standardize on seconds for Nitpick and Sledgehammer timeouts
Tue, 03 Aug 2010 17:43:15 +0200 blanchet speed up Nitpick examples a little bit
Fri, 23 Apr 2010 23:35:43 +0200 wenzelm mark schematic statements explicitly;
Mon, 01 Mar 2010 17:45:02 +0100 wenzelm repaired 'definition' (cf. d8d7d1b785af);
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Wed, 24 Feb 2010 11:55:52 +0100 blanchet compile
Wed, 24 Feb 2010 11:35:10 +0100 blanchet compile
Wed, 24 Feb 2010 09:59:54 +0100 blanchet got rid of "axclass", apparently
Mon, 22 Feb 2010 19:31:00 +0100 blanchet enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
Wed, 10 Feb 2010 11:47:33 +0100 blanchet make Nitpick test a bit weaker;
Tue, 09 Feb 2010 16:07:51 +0100 blanchet optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
Fri, 05 Feb 2010 14:27:21 +0100 blanchet added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
Mon, 14 Dec 2009 10:59:46 +0100 blanchet make Nitpick tests more robust by specifying SAT solver, singlethreading (in Kodkod, not in Isabelle), and higher time limits
Tue, 17 Nov 2009 13:51:16 +0100 blanchet use SAT solver that's available everywhere for this example
Fri, 23 Oct 2009 18:59:24 +0200 blanchet continuation of Nitpick's integration into Isabelle;
less more (0) tip