nominal2: File revisions

Quot/Nominal/LFex.thy

2010-02-23	Cezary Kaliszyk	All works in LF but will require renaming.	file \| diff \| annotate
2010-02-23	Cezary Kaliszyk	Reordering in LF.	file \| diff \| annotate
2010-02-22	Cezary Kaliszyk	Generalize atom_trans and atom_sym.	file \| diff \| annotate
2010-02-12	Cezary Kaliszyk	renamed 'as' to 'is' everywhere.	file \| diff \| annotate
2010-02-11	Cezary Kaliszyk	Notation available locally	file \| diff \| annotate
2010-02-11	Cezary Kaliszyk	Main renaming + fixes for new Isabelle in IntEx2.	file \| diff \| annotate
2010-02-08	Cezary Kaliszyk	Proper context fixes lifting inside instantiations.	file \| diff \| annotate
2010-02-08	Cezary Kaliszyk	Fixed the context import/export and simplified LFex.	file \| diff \| annotate
2010-02-03	Christian Urban	another adaptation for the eqvt-change	file \| diff \| annotate
2010-02-03	Cezary Kaliszyk	The alpha-equivalence relation for let-rec. Not sure if correct...	file \| diff \| annotate
2010-02-02	Cezary Kaliszyk	LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.	file \| diff \| annotate
2010-02-02	Cezary Kaliszyk	With induct instead of induct_tac, just one induction is sufficient.	file \| diff \| annotate
2010-02-02	Cezary Kaliszyk	General alpha_gen_trans for one-variable abstraction.	file \| diff \| annotate
2010-02-01	Cezary Kaliszyk	The current state of fv vs supp proofs in LF.	file \| diff \| annotate

nominal2