src/HOL/Nitpick_Examples/Hotel_Nits.thy
Fri, 06 Dec 2013 09:42:13 +0100 blanchet reverted 86e0b402994c, which was accidentally qfinish'ed and pushed
Thu, 05 Dec 2013 13:38:20 +0100 blanchet experiment
Tue, 03 Jan 2012 18:33:17 +0100 blanchet reintroduced failing examples now that they work again, after reintroduction of "set"
Wed, 21 Sep 2011 15:55:16 +0200 blanchet reintroduced Minipick as Nitpick example
Sat, 23 Apr 2011 13:00:19 +0200 wenzelm modernized specifications;
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.
Tue, 21 Dec 2010 13:57:19 +0100 blanchet show the relation
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
Mon, 22 Feb 2010 19:31:00 +0100 blanchet enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
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
less more (0) tip