src/HOL/Lambda/InductTermi.thy
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2008-01-25 wenzelm 2008-01-25 tuned document;
2007-07-11 berghofe 2007-07-11 - Renamed inductive2 to inductive - Renamed some theorems about transitive closure for predicates
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2005-12-23 wenzelm 2005-12-23 tuned proofs;
2005-11-23 wenzelm 2005-11-23 tuned induction proofs;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2001-10-31 wenzelm 2001-10-31 tuned notation (degree instead of dollar);
2001-10-26 wenzelm 2001-10-26 tuned;
2001-09-28 wenzelm 2001-09-28 tuned;
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-31 wenzelm 2000-08-31 ported HOL/Lambda/ListBeta;
2000-08-29 wenzelm 2000-08-29 Lambda/InductTermi made new-style theory; tuned;
2000-06-21 wenzelm 2000-06-21 fixed deps;
1998-10-21 berghofe 1998-10-21 Changed syntax of inductive.
1998-08-06 nipkow 1998-08-06 First steps towards termination of simply typed terms.