src/HOL/Lambda/WeakNorm.thy
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Wed, 02 Feb 2005 18:20:31 +0100 berghofe Replaced application of subst by simplesubst in proof of app_Var_NF
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