nominal2: File revisions

Nominal/Ex/LamTest.thy

Mon, 19 May 2014 12:45:26 +0100	Christian Urban	changed nominal_primrec into the more appropriate nominal_function	file \| diff \| annotate
Tue, 03 Jan 2012 11:43:27 +0000	Christian Urban	updated to explicit set type constructor (post Isabelle 3rd January)	file \| diff \| annotate
Mon, 17 Jan 2011 12:33:37 +0000	Christian Urban	eliminated tracing code; added flag so that equivariance is only proved for the function graph, not the relation	file \| diff \| annotate
Sat, 15 Jan 2011 21:16:15 +0000	Christian Urban	subst also works now	file \| diff \| annotate
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

nominal2