Nominal/Fv.thy
Wed, 17 Mar 2010 17:40:14 +0100 Cezary Kaliszyk Proper compose_sym2
Wed, 17 Mar 2010 17:09:01 +0100 Cezary Kaliszyk Trying to find a compose lemma for 2 arguments.
Wed, 17 Mar 2010 12:18:35 +0100 Cezary Kaliszyk cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
Wed, 17 Mar 2010 09:57:54 +0100 Cezary Kaliszyk Fix in alpha; support of the recursive Let works :)
Wed, 17 Mar 2010 09:17:55 +0100 Cezary Kaliszyk Generate compound FV and Alpha for recursive bindings.
Tue, 16 Mar 2010 20:07:13 +0100 Cezary Kaliszyk Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not.
Tue, 16 Mar 2010 18:18:08 +0100 Cezary Kaliszyk The old recursive alpha works fine.
less more (0) -30 -10 -7 tip