src/HOL/Lambda/StrongNorm.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 Adapted to new inductive definition package.
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';
2005-11-25 wenzelm 2005-11-25 tuned induct proofs;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2003-06-24 berghofe 2003-06-24 Moved strong normalization proof to StrongNorm.thy