nominal2: Changelog

Christian Urban <urbanc@in.tum.de> [Thu, 04 Feb 2010 15:16:34 +0100] rev 1061

linked versions - instead of copies

Christian Urban <urbanc@in.tum.de> [Thu, 04 Feb 2010 14:55:52 +0100] rev 1060

merged

Christian Urban <urbanc@in.tum.de> [Thu, 04 Feb 2010 14:55:21 +0100] rev 1059

restored the old behaviour of having an eqvts list; the transformed theorems are stored in eqvts_raw

Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Feb 2010 18:28:50 +0100] rev 1058

More let-rec experiments

Christian Urban <urbanc@in.tum.de> [Wed, 03 Feb 2010 17:36:25 +0100] rev 1057

proposal for an alpha equivalence

Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Feb 2010 15:17:29 +0100] rev 1056

Lets different.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Feb 2010 14:39:19 +0100] rev 1055

Simplified the proof.

Christian Urban <urbanc@in.tum.de> [Wed, 03 Feb 2010 14:36:48 +0100] rev 1054

merged

Christian Urban <urbanc@in.tum.de> [Wed, 03 Feb 2010 14:36:22 +0100] rev 1053

proved that bv for lists respects alpha for terms

Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Feb 2010 14:28:00 +0100] rev 1052

Finished remains on the let proof.

nominal2