Nominal/Lift.thy
2010-05-03 Cezary Kaliszyk Move old fv_alpha_export to Fv.
2010-05-02 Christian Urban attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)
2010-04-14 Cezary Kaliszyk Fix the 'subscript' error.
2010-04-14 Cezary Kaliszyk merge
2010-04-14 Cezary Kaliszyk Separate alpha_definition.
2010-04-14 Cezary Kaliszyk Fix spelling in theory header
2010-04-14 Cezary Kaliszyk Initial cleaning/reorganization in Fv.
2010-04-04 Christian Urban separated general nominal theory into separate folder
2010-03-27 Cezary Kaliszyk Lets finally abstract lists.
2010-03-27 Cezary Kaliszyk Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
2010-03-27 Cezary Kaliszyk Get lifted types information from the quotient package.
2010-03-26 Cezary Kaliszyk Removed remaining cheats + some cleaning.
2010-03-19 Cezary Kaliszyk Automatically derive support for datatypes with at-most one binding per constructor.
2010-03-18 Cezary Kaliszyk Rename bound variables + minor cleaning.
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