nominal2: Changelog

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 11:36:03 +0100] rev 1508

Simplified the description.

Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 11:33:56 +0100] rev 1507

merged

Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 11:33:37 +0100] rev 1506

slightly more in the paper

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 11:29:12 +0100] rev 1505

Update the description of the generation of fv function.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 11:16:53 +0100] rev 1504

fv_bn may need to call other fv_bns.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 10:15:57 +0100] rev 1503

Update TODO.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Mar 2010 10:12:41 +0100] rev 1502

Which proofs need a 'sorry'.

Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 10:05:36 +0100] rev 1501

added TODO

Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 10:02:21 +0100] rev 1500

vixed variable names

Christian Urban <urbanc@in.tum.de> [Thu, 18 Mar 2010 09:31:31 +0100] rev 1499

simplified strong induction proof by using flip

nominal2