Nominal/ExLet.thy
2010-04-02 Christian Urban more on the lifting section
2010-04-01 Cezary Kaliszyk fv_fv_bn
2010-04-01 Cezary Kaliszyk fv_perm_bn
2010-04-01 Christian Urban more on the paper
2010-03-31 Christian Urban a test with let having multiple bodies
2010-03-27 Cezary Kaliszyk Lets finally abstract lists.
2010-03-26 Cezary Kaliszyk Fixed renamings.
2010-03-26 Cezary Kaliszyk Removed another cheat and cleaned the code a bit.
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 Properly defined permute_bn. No more sorry's in Let strong induction.
2010-03-25 Cezary Kaliszyk Showed Let substitution.
less more (0) -12 tip