src/HOL/Induct/QuoNestedDataType.thy
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