src/HOL/Lambda/WeakNorm.thy
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-12-23 wenzelm 2005-12-23 tuned proofs;
2005-12-02 berghofe 2005-12-02 Factored out proof for normalization of applications (norm_list).
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-08-25 berghofe 2005-08-25 Adapted to new code generator syntax.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-10 paulson 2005-05-10 oops...cannot use subst here
2005-05-09 paulson 2005-05-09 from simplesubst to new subst
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-02 berghofe 2005-02-02 Replaced application of subst by simplesubst in proof of app_Var_NF to avoid problems with program extraction.
2004-10-11 nipkow 2004-10-11 Proofs needed to be updated because induction now preserves name of induction variable.
2004-06-01 berghofe 2004-06-01 Adapted to new name mangling function in code generator.
2003-06-24 berghofe 2003-06-24 New proof of weak normalization with program extraction.