Quot/Nominal/Terms.thy
2010-02-24 Cezary Kaliszyk Simplified and finised eqvt proofs for t1 and t5
2010-02-24 Cezary Kaliszyk Define lifted perms.
2010-02-24 Cezary Kaliszyk With permute_rsp we can lift the instance proofs :).
2010-02-24 Cezary Kaliszyk Regularize finite support proof for trm1
2010-02-23 Cezary Kaliszyk rsp for bv; the only issue is that it requires an appropriate induction principle.
2010-02-23 Cezary Kaliszyk rsp infrastructure.
2010-02-23 Cezary Kaliszyk Progress towards automatic rsp of constants and fv.
2010-02-23 Cezary Kaliszyk Looking at proving the rsp rules automatically.
2010-02-23 Cezary Kaliszyk Define the quotient from ML
2010-02-23 Cezary Kaliszyk Fixes for auxiliary datatypes.
2010-02-22 Cezary Kaliszyk Fixed pseudo_injectivity for trm4
2010-02-22 Cezary Kaliszyk Testing auto equivp code.
2010-02-22 Cezary Kaliszyk A tactic for final equivp
2010-02-22 Cezary Kaliszyk More equivp infrastructure.
less more (0) -14 tip