Quot/Nominal/LFex.thy
2010-02-01 Cezary Kaliszyk More proofs in the LF example.
2010-02-01 Cezary Kaliszyk Ported LF to the generic lambda and solved the simpler _supp cases.
2010-01-29 Cezary Kaliszyk More in the LF example in the new nominal way, all is clear until support.
2010-01-29 Cezary Kaliszyk Fixed the induction problem + some more proofs.
2010-01-29 Cezary Kaliszyk equivariance of rfv and alpha.
2010-01-29 Cezary Kaliszyk Added the experiments with fun and function.
2010-01-28 Cezary Kaliszyk Ported existing part of LF to new permutations and alphas.
less more (0) tip