Nominal/LFex.thy
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