src/HOL/Lambda/Standardization.thy
2007-10-19 wenzelm 2007-10-19 tuned proofs: avoid implicit prems;
2007-09-06 berghofe 2007-09-06 New proof of standardization theorem (inspired by Ralph Matthes).