Nominal/Term1.thy
2010-03-12 Cezary Kaliszyk Still don't know how to prove supp=fv for simplest Let...
2010-03-11 Cezary Kaliszyk Finite_support proof no longer needed in LF.
2010-03-11 Cezary Kaliszyk Show that the new types are in finite support typeclass.
2010-03-11 Cezary Kaliszyk Fixes for term1 for new alpha. Still not able to show support equations.
2010-03-10 Cezary Kaliszyk alpha_eqvt for recursive term1.
2010-03-08 Cezary Kaliszyk Undo effects of simp.
2010-03-05 Cezary Kaliszyk Still unable to show supp=fv for let with one existential.
2010-03-05 Cezary Kaliszyk Not much progress about the single existential let case.
less more (0) -10 -8 tip