nominal2: File revisions

Nominal/Nominal2_Abs.thy

Tue, 18 Jan 2011 11:02:57 +0100	Christian Urban	the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions	file \| diff \| annotate
Tue, 18 Jan 2011 06:55:18 +0100	Christian Urban	modified the renaming_perm lemmas	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
Fri, 14 Jan 2011 14:22:25 +0000	Christian Urban	strengthened renaming lemmas	file \| diff \| annotate
Mon, 03 Jan 2011 16:19:27 +0000	Christian Urban	simple cases for string rule inductions	file \| diff \| annotate
Tue, 21 Dec 2010 10:28:08 +0000	Christian Urban	all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code	file \| diff \| annotate
Thu, 16 Dec 2010 08:42:48 +0000	Christian Urban	simple cases for strong inducts done; infrastructure for the difficult ones is there	file \| diff \| annotate

nominal2