nominal2: Changelog

Christian Urban <urbanc@in.tum.de> [Tue, 26 Jan 2010 01:42:46 +0100] rev 935

cleaning of QuotProd; a little cleaning of QuotList

Christian Urban <urbanc@in.tum.de> [Tue, 26 Jan 2010 01:00:35 +0100] rev 934

added prs and rsp lemmas for Inl and Inr

Christian Urban <urbanc@in.tum.de> [Tue, 26 Jan 2010 00:47:40 +0100] rev 933

used split_option_all lemma

Christian Urban <urbanc@in.tum.de> [Tue, 26 Jan 2010 00:18:48 +0100] rev 932

used the internal Option.map instead of custom option_map

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 26 Jan 2010 09:54:43 +0100] rev 931

Generalized split_prs and split_rsp

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 26 Jan 2010 09:28:32 +0100] rev 930

All eq_reflections apart from the one of 'id_apply' can be removed.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 26 Jan 2010 08:55:55 +0100] rev 929

continued

nominal2