Nominal/Rsp.thy
2010-03-27 Cezary Kaliszyk Get lifted types information from the quotient package.
2010-03-27 Cezary Kaliszyk New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
2010-03-27 Cezary Kaliszyk Initial proof modifications for alpha_res
2010-03-26 Cezary Kaliszyk Removed remaining cheats + some cleaning.
2010-03-26 Cezary Kaliszyk Removed another cheat and cleaned the code a bit.
2010-03-25 Cezary Kaliszyk Gathering things to prove by induction together; removed cheat_bn_eqvt.
2010-03-24 Cezary Kaliszyk Export all the cheats needed for Core Haskell.
2010-03-22 Cezary Kaliszyk Got rid of alpha_bn_rsp_cheat.
2010-03-22 Cezary Kaliszyk alpha_bn_rsp_pre automatized.
2010-03-22 Cezary Kaliszyk fv_rsp proved automatically.
2010-03-20 Cezary Kaliszyk Use 'alpha_bn_refl' to get rid of one of the sorrys.
2010-03-19 Cezary Kaliszyk Automatically derive support for datatypes with at-most one binding per constructor.
2010-03-18 Cezary Kaliszyk Clean 'Lift', start working only on exported things in Parser.
2010-03-17 Cezary Kaliszyk Finished all proofs in Term5 and Term5n.
2010-03-15 Cezary Kaliszyk cheat_alpha_eqvt no longer needed; the proofs work.
less more (0) -15 tip