nominal2: File revisions

Nominal/Ex/LamTest.thy

2011-01-10	Christian Urban	a few lemmas about freshness for at and at_base	file \| diff \| annotate
2011-01-10	Christian Urban	added a property about finite support in the presense of eqvt_at	file \| diff \| annotate
2011-01-09	Christian Urban	instantiated fundef_ex1_eqvt_at theorem with the indction hypothesis	file \| diff \| annotate
2011-01-09	Christian Urban	solved subgoals for depth and subst function	file \| diff \| annotate
2011-01-09	Christian Urban	added eqvt_at premises in function definition - however not proved at the moment	file \| diff \| annotate
2011-01-07	Christian Urban	added one further lemma about equivariance of THE_default	file \| diff \| annotate
2011-01-07	Christian Urban	equivariance of THE_default under the uniqueness assumption	file \| diff \| annotate
2011-01-07	Christian Urban	derived equivariance for the function graph and function relation	file \| diff \| annotate
2011-01-06	Christian Urban	a modified function package where, as a test, True has been injected into the compatibility condictions	file \| diff \| annotate

nominal2