nominal2: File revisions

Quot/Nominal/Abs.thy

2010-02-12	Cezary Kaliszyk	renamed 'as' to 'is' everywhere.	file \| diff \| annotate
2010-02-11	Cezary Kaliszyk	Main renaming + fixes for new Isabelle in IntEx2.	file \| diff \| annotate
2010-02-09	Christian Urban	merged	file \| diff \| annotate
2010-02-09	Christian Urban	a few more attempts to show the equivalence between old and new way of defining alpha-equivalence	file \| diff \| annotate
2010-02-09	Cezary Kaliszyk	Fixed pattern matching, now the test in Abs works correctly.	file \| diff \| annotate
2010-02-08	Christian Urban	added a test case	file \| diff \| annotate
2010-02-08	Christian Urban	moved some lemmas to Nominal; updated all files	file \| diff \| annotate
2010-02-04	Christian Urban	fixed (permute_eqvt in eqvts makes this simpset always looping)	file \| diff \| annotate
2010-02-03	Christian Urban	fixed proofs in Abs.thy	file \| diff \| annotate
2010-02-03	Cezary Kaliszyk	Minor	file \| diff \| annotate
2010-02-02	Cezary Kaliszyk	Disambiguating the syntax.	file \| diff \| annotate
2010-02-02	Cezary Kaliszyk	Some equivariance machinery that comes useful in LF.	file \| diff \| annotate
2010-02-02	Cezary Kaliszyk	General alpha_gen_trans for one-variable abstraction.	file \| diff \| annotate
2010-02-01	Christian Urban	added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case	file \| diff \| annotate
2010-02-01	Christian Urban	cleaned	file \| diff \| annotate

nominal2