Nominal/Term5.thy
2010-03-17 Cezary Kaliszyk Finished all proofs in Term5 and Term5n.
2010-03-16 Cezary Kaliszyk Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not.
2010-03-16 Cezary Kaliszyk The old recursive alpha works fine.
2010-03-16 Cezary Kaliszyk Alpha is wrong.
2010-03-16 Cezary Kaliszyk alpha5_transp and equivp
2010-03-16 Cezary Kaliszyk alpha5_symp proved.
2010-03-16 Cezary Kaliszyk FV_bn generated for recursive functions as well, and used in main fv for bindings.
2010-03-16 Cezary Kaliszyk The proof in 'Test' gets simpler.
2010-03-11 Cezary Kaliszyk looking at trm5_equivp
2010-03-11 Cezary Kaliszyk The alpha5_eqvt tactic works if I manage to build the goal.
2010-03-10 Cezary Kaliszyk More tries about the proofs in trm5
2010-03-10 Cezary Kaliszyk alpha_equivp for trm5
2010-03-10 Cezary Kaliszyk Looking at alpha_eqvt for term5, not much progress.
2010-03-10 Cezary Kaliszyk Testing equalities in trm5, all seems good.
2010-03-01 Cezary Kaliszyk The new alpha-equivalence and testing in Trm2 and Trm5.
2010-03-01 Christian Urban slight simplification of the raw-decl generation
2010-03-01 Cezary Kaliszyk Example that shows that current alpha is wrong.
2010-02-26 Cezary Kaliszyk Permutation and FV_Alpha interface change.
2010-02-25 Cezary Kaliszyk Split Terms into separate files and add them to tests.
less more (0) tip