src/HOL/Library/Coinductive_List.thy
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2007-12-10 haftmann 2007-12-10 switched import from Main to List
2007-10-05 wenzelm 2007-10-05 tuned proofs (via polymorphic taking'');
2007-10-05 wenzelm 2007-10-05 coinduct: instantiation refers to suffix of main prop (major premise or conclusion); tuned;
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2007-04-24 berghofe 2007-04-24 Adapted to new parse translation for case expressions.
2007-02-27 wenzelm 2007-02-27 tuned document;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-10-01 wenzelm 2006-10-01 removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
2006-09-30 wenzelm 2006-09-30 tuned proofs;
2006-09-28 wenzelm 2006-09-28 fixed translations: CONST;
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2006-02-16 wenzelm 2006-02-16 new-style definitions/abbreviations;
2006-01-21 wenzelm 2006-01-21 tuned proofs;
2005-12-13 wenzelm 2005-12-13 Potentially infinite lists as greatest fixed-point.