nominal2: File revisions

Nominal/Nominal2_Eqvt.thy

Mon, 17 Jan 2011 17:20:21 +0100	Christian Urban	added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)	file \| diff \| annotate
Mon, 17 Jan 2011 12:34:11 +0000	Christian Urban	moved high level code from LamTest into the main libraries.	file \| diff \| annotate
Thu, 13 Jan 2011 12:12:47 +0000	Christian Urban	added eqvt_lemmas for subset and psubset	file \| diff \| annotate
Fri, 07 Jan 2011 05:06:25 +0000	Christian Urban	equivariance of THE_default under the uniqueness assumption	file \| diff \| annotate
Thu, 06 Jan 2011 13:28:19 +0000	Christian Urban	same	file \| diff \| annotate
Mon, 03 Jan 2011 16:19:27 +0000	Christian Urban	simple cases for string rule inductions	file \| diff \| annotate
Mon, 29 Nov 2010 08:01:09 +0000	Christian Urban	isarfied some of the high-level proofs	file \| diff \| annotate
Sun, 14 Nov 2010 16:34:47 +0000	Christian Urban	merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy	file \| diff \| annotate \| base

nominal2