nominal2: Changelog

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 28 Jun 2011 14:30:30 +0900] rev 2920

Leftover only inj and eqvt

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 28 Jun 2011 14:18:26 +0900] rev 2919

eapply fcb ok

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 28 Jun 2011 14:01:15 +0900] rev 2918

Removed Inl and Inr

Christian Urban <urbanc@in.tum.de> [Tue, 28 Jun 2011 14:49:48 +0100] rev 2917

relaxed type in fcb

Christian Urban <urbanc@in.tum.de> [Tue, 28 Jun 2011 14:34:07 +0100] rev 2916

fcb with explicit bn function

Christian Urban <urbanc@in.tum.de> [Tue, 28 Jun 2011 14:01:52 +0100] rev 2915

added let-rec example

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 28 Jun 2011 12:36:34 +0900] rev 2914

Experiments with res

Christian Urban <urbanc@in.tum.de> [Tue, 28 Jun 2011 00:48:57 +0100] rev 2913

proved the fcb also for sets (no restriction yet)

Christian Urban <urbanc@in.tum.de> [Tue, 28 Jun 2011 00:30:30 +0100] rev 2912

copied all work to Lambda.thy; had to derive a special version of fcb1 for concrete atom

Christian Urban <urbanc@in.tum.de> [Mon, 27 Jun 2011 22:51:42 +0100] rev 2911

streamlined the fcb-proof and made fcb1 a special case of fcb

nominal2