nominal2: File revisions

Nominal/Rsp.thy

2010-05-03	Cezary Kaliszyk	alpha_eqvt_tac fixed to work when the existential is not at the top level.	file \| diff \| annotate
2010-04-19	Christian Urban	deleting function perm_arg in favour of the library function mk_perm	file \| diff \| annotate
2010-04-19	Cezary Kaliszyk	Accept non-equality eqvt rules in support proofs.	file \| diff \| annotate
2010-04-01	Cezary Kaliszyk	Let with multiple bindings.	file \| diff \| annotate
2010-03-27	Cezary Kaliszyk	Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.	file \| diff \| annotate
2010-03-27	Cezary Kaliszyk	Get lifted types information from the quotient package.	file \| diff \| annotate
2010-03-27	Cezary Kaliszyk	New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.	file \| diff \| annotate
2010-03-27	Cezary Kaliszyk	Initial proof modifications for alpha_res	file \| diff \| annotate
2010-03-26	Cezary Kaliszyk	Removed remaining cheats + some cleaning.	file \| diff \| annotate
2010-03-26	Cezary Kaliszyk	Removed another cheat and cleaned the code a bit.	file \| diff \| annotate
2010-03-25	Cezary Kaliszyk	Gathering things to prove by induction together; removed cheat_bn_eqvt.	file \| diff \| annotate
2010-03-24	Cezary Kaliszyk	Export all the cheats needed for Core Haskell.	file \| diff \| annotate

nominal2