| Wed, 02 May 2007 01:42:23 +0200 | urbanc | tuned some proofs and changed variable names in some definitions of Nominal.thy | file | diff | annotate |
| Wed, 28 Mar 2007 18:25:23 +0200 | urbanc | the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive | file | diff | annotate |
| Tue, 06 Mar 2007 15:28:22 +0100 | urbanc | major update of the nominal package; there is now an infrastructure | file | diff | annotate |
| Wed, 07 Feb 2007 17:44:07 +0100 | berghofe | Adapted to new inductive definition package. | file | diff | annotate |
| Mon, 27 Nov 2006 12:11:43 +0100 | berghofe | Adapted to new nominal_primrec command. | file | diff | annotate |
| Mon, 23 Oct 2006 00:51:16 +0200 | berghofe | Adapted to changes in FCBs. | file | diff | annotate |
| Tue, 10 Oct 2006 16:26:59 +0200 | urbanc | made some proof look more like the ones in Barendregt | file | diff | annotate |