src/HOL/Lambda/WeakNorm.thy
Mon, 11 Oct 2004 07:42:22 +0200 nipkow Proofs needed to be updated because induction now preserves name of
Tue, 01 Jun 2004 15:00:26 +0200 berghofe Adapted to new name mangling function in code generator.
Tue, 24 Jun 2003 10:37:12 +0200 berghofe New proof of weak normalization with program extraction.
less more (0) tip