Nominal/Lift.thy
2010-03-18 Cezary Kaliszyk Move most of the exporting out of the parser.
2010-03-18 Cezary Kaliszyk Clean 'Lift', start working only on exported things in Parser.
2010-03-04 Cezary Kaliszyk Lift distinct.
2010-03-02 Cezary Kaliszyk Porting from Lift to Parser; until defining the Quotient type.
2010-03-02 Cezary Kaliszyk Working bv_eqvt
2010-03-02 Cezary Kaliszyk More fixes for new alpha, the whole lift script should now work again.
2010-03-01 Cezary Kaliszyk Trying to prove equivariance.
2010-02-26 Cezary Kaliszyk More about the general lifting procedure.
2010-02-26 Cezary Kaliszyk Progress with general lifting procedure.
2010-02-26 Cezary Kaliszyk Permutation and FV_Alpha interface change.
2010-02-26 Cezary Kaliszyk To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.
2010-02-25 Cezary Kaliszyk Preparing the generalized lifting procedure
less more (0) tip