2010-03-27 Cezary Kaliszyk Minor fix.
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-27 Cezary Kaliszyk merge
2010-03-27 Cezary Kaliszyk Fv/Alpha now takes into account Alpha_Type given from the parser.
2010-03-27 Cezary Kaliszyk Minor cleaning.
2010-03-27 Christian Urban merged
2010-03-27 Christian Urban more on the paper
2010-03-27 Cezary Kaliszyk Removed some warnings.
2010-03-26 Cezary Kaliszyk merge
2010-03-26 Cezary Kaliszyk Modified abs_gen_sym and abs_gen_trans so it becomes usable in the proofs.
2010-03-26 Christian Urban merged
2010-03-26 Christian Urban more on the paper
2010-03-26 Christian Urban simplification
2010-03-26 Cezary Kaliszyk merge
2010-03-26 Cezary Kaliszyk Describe 'nominal_datatype2'.
2010-03-26 Cezary Kaliszyk Fixed renamings.
2010-03-26 Christian Urban merged
2010-03-26 Cezary Kaliszyk Removed remaining cheats + some cleaning.
2010-03-26 Cezary Kaliszyk Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
2010-03-26 Cezary Kaliszyk Update cheats in TODO.
2010-03-26 Cezary Kaliszyk Removed another cheat and cleaned the code a bit.
2010-03-26 Cezary Kaliszyk Fix Manual/LamEx for experiments.
2010-03-25 Cezary Kaliszyk Proper bn_rsp, for bn functions calling each other.
2010-03-25 Cezary Kaliszyk Gathering things to prove by induction together; removed cheat_bn_eqvt.
2010-03-25 Cezary Kaliszyk Update TODO
2010-03-25 Cezary Kaliszyk Showed ACons_subst.
2010-03-25 Cezary Kaliszyk Only ACons_subst left to show.
(0) -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 tip