nominal2: File revisions

Nominal/Ex/LamTest.thy

Sat, 15 Jan 2011 20:24:16 +0000	Christian Urban	nominal_function works now completely for frees and depth; still a propbelm with subst; no unproved assumptions	file \| diff \| annotate
Mon, 10 Jan 2011 11:36:55 +0000	Christian Urban	a few lemmas about freshness for at and at_base	file \| diff \| annotate
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

nominal2