src/HOL/Induct/QuoNestedDataType.thy
Fri, 01 Oct 2010 16:05:25 +0200 haftmann constant `contents` renamed to `the_elem`
Wed, 08 Sep 2010 19:21:46 +0200 haftmann modernized primrec
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Mon, 02 Mar 2009 16:53:55 +0100 nipkow name changes
Wed, 11 Jul 2007 11:14:51 +0200 berghofe Adapted to new inductive definition package.
Wed, 07 Feb 2007 17:39:49 +0100 berghofe Adapted to changes in List theory.
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Tue, 07 Nov 2006 11:47:57 +0100 wenzelm renamed 'const_syntax' to 'notation';
Wed, 13 Sep 2006 12:05:50 +0200 krauss Major update to function package, including new syntax and the (only theoretical)
Sat, 27 May 2006 17:42:02 +0200 wenzelm tuned;
Thu, 22 Dec 2005 00:28:43 +0100 wenzelm tuned induct proofs;
Wed, 21 Dec 2005 12:02:57 +0100 paulson removed or modified some instances of [iff]
Thu, 24 Nov 2005 00:00:20 +0100 wenzelm tuned induct proofs;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Thu, 02 Sep 2004 16:52:21 +0200 paulson new example of a quotiented nested data type
less more (0) tip