| Thu, 25 Aug 2005 16:13:09 +0200 | berghofe | Adapted to new code generator syntax. | file | diff | annotate |
| Fri, 17 Jun 2005 16:12:49 +0200 | haftmann | migrated theory headers to new format | file | diff | annotate |
| Tue, 10 May 2005 10:25:21 +0200 | paulson | oops...cannot use subst here | file | diff | annotate |
| Mon, 09 May 2005 16:38:56 +0200 | paulson | from simplesubst to new subst | file | diff | annotate |
| Thu, 03 Mar 2005 12:43:01 +0100 | skalberg | Move towards standard functions. | file | diff | annotate |
| Wed, 02 Feb 2005 18:20:31 +0100 | berghofe | Replaced application of subst by simplesubst in proof of app_Var_NF | file | diff | annotate |
| Mon, 11 Oct 2004 07:42:22 +0200 | nipkow | Proofs needed to be updated because induction now preserves name of | file | diff | annotate |
| Tue, 01 Jun 2004 15:00:26 +0200 | berghofe | Adapted to new name mangling function in code generator. | file | diff | annotate |
| Tue, 24 Jun 2003 10:37:12 +0200 | berghofe | New proof of weak normalization with program extraction. | file | diff | annotate |