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