src/HOL/Lambda/Eta.thy
2008-02-28 wenzelm 2008-02-28 Transitive_Closure: induct and cases rules now declare proper case_names;
2008-01-25 wenzelm 2008-01-25 tuned document; modernized primrec;
2007-08-12 wenzelm 2007-08-12 added type constraints to resolve syntax ambiguities;
2007-07-11 berghofe 2007-07-11 - Renamed inductive2 to inductive - Renamed some theorems about transitive closure for predicates
2007-03-09 haftmann 2007-03-09 stepping towards uniform lattice theory development in HOL
2007-02-07 berghofe 2007-02-07 - Adapted to new inductive definition package - More elegant proof of eta postponement theorem inspired by Andreas Abel
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-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax;
2006-04-09 wenzelm 2006-04-09 tuned syntax/abbreviations;
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-02-16 wenzelm 2006-02-16 new-style definitions/abbreviations;
2006-01-03 paulson 2006-01-03 Provers/classical: stricter checks to ensure that supplied intro, dest and elim rules are well-formed
2005-12-22 wenzelm 2005-12-22 tuned induct proofs;
2005-11-25 wenzelm 2005-11-25 tuned induct proofs;
2005-11-23 wenzelm 2005-11-23 tuned induction proofs;
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-02-10 berghofe 2005-02-10 Added proof of eta-postponement theorem (using parallel eta-reduction).
2002-05-30 nipkow 2002-05-30 Modifications due to enhanced linear arithmetic.
2001-10-31 wenzelm 2001-10-31 tuned notation (degree instead of dollar);
2001-09-28 wenzelm 2001-09-28 inductive: no collective atts;
2001-02-26 paulson 2001-02-26 minor tweaks to speed the proofs
2000-09-12 wenzelm 2000-09-12 renamed atts: rulify to rule_format, elimify to elim_format;
2000-09-07 wenzelm 2000-09-07 updated attribute names;
2000-09-05 wenzelm 2000-09-05 use 'iff' modifier;
2000-09-04 wenzelm 2000-09-04 tuned;
2000-09-02 wenzelm 2000-09-02 HOL/Lambda: converted into new-style theory and document;
2000-06-21 wenzelm 2000-06-21 fixed deps;
1999-03-08 nipkow 1999-03-08 Suc -> +1
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-15 nipkow 1998-07-15 @ -> $
1996-11-04 nipkow 1996-11-04 Used nat_trans_tac. New Eta. various smaller changes.
1996-08-08 berghofe 1996-08-08 Simplified primrec definitions.
1996-06-06 paulson 1996-06-06 Quotes now optional around inductive set
1995-12-01 clasohm 1995-12-01 removed quotes from consts and syntax sections
1995-10-06 nipkow 1995-10-06 New version with eta reduction.