src/HOL/Induct/QuoNestedDataType.thy
2010-10-01 haftmann 2010-10-01 constant `contents` renamed to `the_elem`
2010-09-08 haftmann 2010-09-08 modernized primrec
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-03-02 nipkow 2009-03-02 name changes
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2007-02-07 berghofe 2007-02-07 Adapted to changes in List theory.
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-09-13 krauss 2006-09-13 Major update to function package, including new syntax and the (only theoretical) ability to handle local contexts.
2006-05-27 wenzelm 2006-05-27 tuned;
2005-12-22 wenzelm 2005-12-22 tuned induct proofs;
2005-12-21 paulson 2005-12-21 removed or modified some instances of [iff]
2005-11-24 wenzelm 2005-11-24 tuned induct proofs;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-09-02 paulson 2004-09-02 new example of a quotiented nested data type