Nominal/LFex.thy
2010-03-16 Cezary Kaliszyk FV_bn generated for recursive functions as well, and used in main fv for bindings.
2010-03-15 Cezary Kaliszyk LF works with new alpha...?
2010-03-11 Cezary Kaliszyk Finite_support proof no longer needed in LF.
2010-03-08 Cezary Kaliszyk More fine-grained nominal restriction for debugging.
2010-03-05 Cezary Kaliszyk Ported LF to the parser interface.
2010-03-05 Cezary Kaliszyk Fixed LF for one quantifier over 2 premises.
2010-03-02 Cezary Kaliszyk Minor
2010-03-02 Cezary Kaliszyk Fixed eqvt code.
2010-02-26 Cezary Kaliszyk RSP of perms can be shown in one go.
2010-02-26 Cezary Kaliszyk Change in signature of prove_const_rsp for general lifting.
2010-02-26 Cezary Kaliszyk Permutation and FV_Alpha interface change.
2010-02-25 Cezary Kaliszyk Code for proving eqvt, still in Terms.
2010-02-25 Christian Urban merged
2010-02-25 Christian Urban moved Nominal to "toplevel"
less more (0) tip