Nominal/Term1.thy
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.
Fri, 12 Mar 2010 12:42:35 +0100 Cezary Kaliszyk Still don't know how to prove supp=fv for simplest Let...
Thu, 11 Mar 2010 17:49:07 +0100 Cezary Kaliszyk Finite_support proof no longer needed in LF.
Thu, 11 Mar 2010 17:47:29 +0100 Cezary Kaliszyk Show that the new types are in finite support typeclass.
Thu, 11 Mar 2010 16:15:29 +0100 Cezary Kaliszyk Fixes for term1 for new alpha. Still not able to show support equations.
Wed, 10 Mar 2010 15:32:51 +0100 Cezary Kaliszyk alpha_eqvt for recursive term1.
Mon, 08 Mar 2010 02:40:16 +0100 Cezary Kaliszyk Undo effects of simp.
Fri, 05 Mar 2010 18:14:04 +0100 Cezary Kaliszyk Still unable to show supp=fv for let with one existential.
less more (0) -10 -8 tip