src/HOL/Lambda/ListApplication.thy
2007-06-21 wenzelm 2007-06-21 tuned proofs -- avoid implicit prems;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
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-06-17 haftmann 2005-06-17 migrated theory headers to new format
2003-06-24 berghofe 2003-06-24 Added lift_map and subst_map.
2003-04-23 berghofe 2003-04-23 Eliminated most occurrences of rule_format attribute.
2001-10-31 wenzelm 2001-10-31 tuned notation (degree instead of dollar);
2001-10-26 wenzelm 2001-10-26 tuned;
2001-10-26 wenzelm 2001-10-26 tuned notation;
2001-09-04 wenzelm 2001-09-04 renamed "antecedent" case to "rule_context";
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-06 nipkow 2000-09-06 less_induct -> nat_less_induct
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-06-21 wenzelm 2000-06-21 fixed deps;
1998-08-06 nipkow 1998-08-06 First steps towards termination of simply typed terms.