Nominal/Nominal2_Eqvt.thy
2011-01-19 Christian Urban added eqvt and supp lemma for removeAll (function from List.thy)
2011-01-18 Christian Urban some tryes about substitution over type-schemes
2011-01-18 Christian Urban removed finiteness assumption from set_rename_perm
2011-01-18 Christian Urban modified the renaming_perm lemmas
2011-01-17 Christian Urban added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
2011-01-17 Christian Urban moved high level code from LamTest into the main libraries.
2011-01-13 Christian Urban added eqvt_lemmas for subset and psubset
2011-01-07 Christian Urban equivariance of THE_default under the uniqueness assumption
2011-01-06 Christian Urban same
2011-01-03 Christian Urban simple cases for string rule inductions
2010-11-29 Christian Urban isarfied some of the high-level proofs
2010-11-14 Christian Urban merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
2010-03-11 Christian Urban finally the proof that new and old alpha agree
2010-03-03 Cezary Kaliszyk Fix eqvt for multiple quantifiers.
2010-03-03 Cezary Kaliszyk weird eqvt
2010-03-02 Cezary Kaliszyk Add image_eqvt and atom_eqvt to eqvt bases.
2010-02-25 Christian Urban moved Nominal to "toplevel"
less more (0) tip