nominal2: File revisions

Nominal/ExLet.thy

2010-04-02	Christian Urban	more on the lifting section	file \| diff \| annotate
2010-04-01	Cezary Kaliszyk	fv_fv_bn	file \| diff \| annotate
2010-04-01	Cezary Kaliszyk	fv_perm_bn	file \| diff \| annotate
2010-04-01	Christian Urban	more on the paper	file \| diff \| annotate
2010-03-31	Christian Urban	a test with let having multiple bodies	file \| diff \| annotate
2010-03-27	Cezary Kaliszyk	Lets finally abstract lists.	file \| diff \| annotate
2010-03-26	Cezary Kaliszyk	Fixed renamings.	file \| diff \| annotate
2010-03-26	Cezary Kaliszyk	Removed another cheat and cleaned the code a bit.	file \| diff \| annotate
2010-03-25	Cezary Kaliszyk	Proper bn_rsp, for bn functions calling each other.	file \| diff \| annotate
2010-03-25	Cezary Kaliszyk	Gathering things to prove by induction together; removed cheat_bn_eqvt.	file \| diff \| annotate
2010-03-25	Cezary Kaliszyk	Properly defined permute_bn. No more sorry's in Let strong induction.	file \| diff \| annotate
2010-03-25	Cezary Kaliszyk	Showed Let substitution.	file \| diff \| annotate

nominal2