nominal2: File revisions

Nominal/Ex/LamTest.thy

Mon, 10 Jan 2011 08:51:51 +0000	Christian Urban	added a property about finite support in the presense of eqvt_at	file \| diff \| annotate
Sun, 09 Jan 2011 05:38:53 +0000	Christian Urban	instantiated fundef_ex1_eqvt_at theorem with the indction hypothesis	file \| diff \| annotate
Sun, 09 Jan 2011 04:28:24 +0000	Christian Urban	solved subgoals for depth and subst function	file \| diff \| annotate
Sun, 09 Jan 2011 01:17:44 +0000	Christian Urban	added eqvt_at premises in function definition - however not proved at the moment	file \| diff \| annotate
Fri, 07 Jan 2011 05:40:31 +0000	Christian Urban	added one further lemma about equivariance of THE_default	file \| diff \| annotate
Fri, 07 Jan 2011 05:06:25 +0000	Christian Urban	equivariance of THE_default under the uniqueness assumption	file \| diff \| annotate
Fri, 07 Jan 2011 02:30:00 +0000	Christian Urban	derived equivariance for the function graph and function relation	file \| diff \| annotate
Thu, 06 Jan 2011 23:06:45 +0000	Christian Urban	a modified function package where, as a test, True has been injected into the compatibility condictions	file \| diff \| annotate

nominal2