src/HOL/Lambda/ListOrder.thy
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 Converted to predicate notation.
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-05-05 krauss 2006-05-05 First usable version of the new function definition package (HOL/function_packake/...). Moved Accessible_Part.thy from Library to Main.
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
2002-09-30 berghofe 2002-09-30 Adapted to new simplifier.
2001-09-28 wenzelm 2001-09-28 tuned;
2000-10-18 wenzelm 2000-10-18 use Accessible_Part from HOL/Library;
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-06-21 wenzelm 2000-06-21 fixed deps;
1998-08-06 nipkow 1998-08-06 First steps towards termination of simply typed terms.