src/HOL/Nitpick_Examples/Core_Nits.thy
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Tue, 06 Oct 2015 15:14:28 +0200 wenzelm fewer aliases for toplevel theorem statements;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Mon, 03 Mar 2014 23:05:30 +0100 blanchet fixed handling of 'case_prod' and other 'case' functions for interpreted types
Wed, 12 Feb 2014 08:35:56 +0100 blanchet removed trivial 'rec' examples for nonrecursive types (I could also have added the 'old.' prefix in front of the constant names)
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:18 +0100 blanchet fixed type annotations
Tue, 03 Jan 2012 18:33:17 +0100 blanchet fixed a few more bugs in \Nitpick's new "set" support
Sat, 24 Dec 2011 15:53:10 +0100 haftmann adjusted to set/pred distinction by means of type constructor `set`
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
less more (0) -15 tip