Nominal/Rsp.thy
2010-04-19 Christian Urban deleting function perm_arg in favour of the library function mk_perm
2010-04-19 Cezary Kaliszyk Accept non-equality eqvt rules in support proofs.
2010-04-01 Cezary Kaliszyk Let with multiple bindings.
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-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.
less more (0) -15 tip