Nominal/Rsp.thy
2010-05-03 Cezary Kaliszyk alpha_eqvt_tac fixed to work when the existential is not at the top level.
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.
less more (0) -12 tip