nominal2: File revisions

Nominal/Ex/Lambda.thy

Tue, 31 May 2011 12:22:28 +0100	Christian Urban	fixed the problem with cps-like functions	file \| diff \| annotate
Tue, 31 May 2011 14:12:31 +0900	Cezary Kaliszyk	DeBruijn translation in a simplifier friendly way	file \| diff \| annotate
Tue, 31 May 2011 13:25:35 +0900	Cezary Kaliszyk	map_term can be defined when equivariance is assumed	file \| diff \| annotate
Tue, 31 May 2011 13:21:00 +0900	Cezary Kaliszyk	map_term is not a function the way it is defined	file \| diff \| annotate
Tue, 31 May 2011 12:59:10 +0900	Cezary Kaliszyk	Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.	file \| diff \| annotate
Tue, 31 May 2011 12:54:21 +0900	Cezary Kaliszyk	Simple eqvt proofs with perm_simps for clarity	file \| diff \| annotate
Tue, 31 May 2011 00:17:22 +0100	Christian Urban	functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition	file \| diff \| annotate
Wed, 25 May 2011 21:38:50 +0200	Christian Urban	added eq_iff and distinct lemmas of nominal datatypes to the simplifier	file \| diff \| annotate

nominal2