src/HOL/Library/Coinductive_List.thy
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2010-01-16 haftmann 2010-01-16 dropped some old primrecs and some constdefs
2009-10-26 wenzelm 2009-10-26 tuned white space;
2009-10-23 blanchet 2009-10-23 continuation of Nitpick's integration into Isabelle; added examples, and integrated non-Main theories better.
2009-10-21 blanchet 2009-10-21 renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-23 blanchet 2009-09-23 Added "nitpick_const_simp" tags to lazy list theories. (Will be useful once Nitpick is integrated in Isabelle.)
2009-04-24 haftmann 2009-04-24 funpow and relpow with shared "^^" syntax
2009-04-20 haftmann 2009-04-20 power operation on functions with syntax o^; power operation on relations with syntax ^^
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-03-02 nipkow 2009-03-02 name changes
2008-11-20 wenzelm 2008-11-20 Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-10-28 haftmann 2008-10-28 removed includes
2008-10-27 haftmann 2008-10-27 added rudimentary code generation
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.