nominal2: File revisions

Nominal/Term1.thy

Mon, 15 Mar 2010 13:56:17 +0100	Cezary Kaliszyk	build_eqvts works with recursive case if proper induction rule is used.	file \| diff \| annotate
Sat, 13 Mar 2010 13:49:15 +0100	Christian Urban	started supp-fv proofs (is going to work)	file \| diff \| annotate
Fri, 12 Mar 2010 17:42:31 +0100	Cezary Kaliszyk	Even with pattern simplified to a single clause, the supp equation doesn't seem true.	file \| diff \| annotate
Fri, 12 Mar 2010 12:42:35 +0100	Cezary Kaliszyk	Still don't know how to prove supp=fv for simplest Let...	file \| diff \| annotate
Thu, 11 Mar 2010 17:49:07 +0100	Cezary Kaliszyk	Finite_support proof no longer needed in LF.	file \| diff \| annotate
Thu, 11 Mar 2010 17:47:29 +0100	Cezary Kaliszyk	Show that the new types are in finite support typeclass.	file \| diff \| annotate
Thu, 11 Mar 2010 16:15:29 +0100	Cezary Kaliszyk	Fixes for term1 for new alpha. Still not able to show support equations.	file \| diff \| annotate
Wed, 10 Mar 2010 15:32:51 +0100	Cezary Kaliszyk	alpha_eqvt for recursive term1.	file \| diff \| annotate

nominal2