nominal2: File revisions

Nominal/Ex/Let.thy

Sat, 02 Jul 2011 00:27:47 +0100	Christian Urban	side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function	file \| diff \| annotate
Wed, 29 Jun 2011 19:21:26 +0100	Christian Urban	moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through	file \| diff \| annotate
Wed, 29 Jun 2011 17:01:09 +0100	Christian Urban	added a warning if a theorem is already declared as equivariant	file \| diff \| annotate
Wed, 29 Jun 2011 16:44:54 +0100	Christian Urban	merged	file \| diff \| annotate
Wed, 29 Jun 2011 13:04:24 +0900	Cezary Kaliszyk	Prove bn injectivity and experiment more with Let	file \| diff \| annotate
Wed, 29 Jun 2011 00:48:50 +0100	Christian Urban	some experiments	file \| diff \| annotate
Tue, 28 Jun 2011 14:45:30 +0900	Cezary Kaliszyk	trying new fcb in let/subst	file \| diff \| annotate
Mon, 20 Jun 2011 09:59:18 +0900	Cezary Kaliszyk	Move lst_fcb to Nominal2_Abs	file \| diff \| annotate

nominal2