nominal2: File revisions

Nominal/Ex/Lambda.thy

2010-08-27	Christian Urban	make copies of the "old" files	file \| diff \| annotate
2010-08-26	Christian Urban	"isabelle make test" makes all major examples....they work up to supp theorems (excluding)	file \| diff \| annotate
2010-08-25	Christian Urban	cleaned up (almost completely) the examples	file \| diff \| annotate
2010-08-25	Christian Urban	automatic lifting	file \| diff \| annotate
2010-08-25	Christian Urban	now every lemma lifts (even with type variables)	file \| diff \| annotate
2010-08-25	Christian Urban	can now deal with type variables in nominal datatype definitions	file \| diff \| annotate
2010-08-21	Christian Urban	nominal_datatypes with type variables do not work	file \| diff \| annotate
2010-08-21	Christian Urban	changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default	file \| diff \| annotate
2010-06-07	Christian Urban	work on transitivity proof	file \| diff \| annotate
2010-05-21	Cezary Kaliszyk	Match_Lam defined on Quotient Level.	file \| diff \| annotate
2010-05-21	Cezary Kaliszyk	More on Function-defined subst.	file \| diff \| annotate
2010-05-21	Cezary Kaliszyk	merge	file \| diff \| annotate
2010-05-21	Cezary Kaliszyk	Renamings.	file \| diff \| annotate
2010-05-21	Cezary Kaliszyk	merge (non-trival)	file \| diff \| annotate
2010-05-21	Cezary Kaliszyk	Previously uncommited direct subst definition changes.	file \| diff \| annotate

nominal2