src/HOL/Lambda/Type.thy
2010-04-23 wenzelm 2010-04-23 mark schematic statements explicitly;
2008-01-25 wenzelm 2008-01-25 modernized primrec;
2007-07-11 berghofe 2007-07-11 - Renamed inductive2 to inductive - Renamed some theorems about transitive closure for predicates
2007-06-21 wenzelm 2007-06-21 tuned proofs -- avoid implicit prems;
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
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-08-09 wenzelm 2006-08-09 tuned proofs;
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;
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
2004-10-11 nipkow 2004-10-11 Proofs needed to be updated because induction now preserves name of induction variable.
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2003-06-24 berghofe 2003-06-24 Moved strong normalization proof to StrongNorm.thy
2002-09-30 nipkow 2002-09-30 modified induct method
2001-11-13 wenzelm 2001-11-13 tuned inductions;
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
2001-10-31 wenzelm 2001-10-31 tuned notation (degree instead of dollar);
2001-10-31 wenzelm 2001-10-31 (induct set: ...);
2001-10-30 wenzelm 2001-10-30 tuned induct proofs;
2001-10-26 berghofe 2001-10-26 Eliminated occurrence of rule_format.
2001-10-26 wenzelm 2001-10-26 tuned;
2001-10-26 wenzelm 2001-10-26 tuned;
2001-10-26 wenzelm 2001-10-26 Rrightarrow;
2001-10-26 wenzelm 2001-10-26 tuned notation;
2001-10-25 berghofe 2001-10-25 Replaced main proof by proper Isar script.
2001-10-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-09-28 wenzelm 2001-09-28 inductive: no collective atts;
2000-12-01 wenzelm 2000-12-01 schematic goals;
2000-10-04 wenzelm 2000-10-04 new 'THEN' syntax;
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-02 wenzelm 2000-09-02 HOL/Lambda: converted into new-style theory and document;
2000-09-01 wenzelm 2000-09-01 converted Lambda scripts;
2000-08-29 wenzelm 2000-08-29 Lambda/InductTermi made new-style theory; tuned;
2000-08-19 wenzelm 2000-08-19 fixed text;
2000-08-17 wenzelm 2000-08-17 tuned;
2000-08-17 wenzelm 2000-08-17 converted to new-style theory;
2000-06-23 berghofe 2000-06-23 Subject reduction and strong normalization of simply-typed lambda terms.