nominal2: Changelog

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Mar 2010 12:04:38 +0100] rev 1646

Solved all boring subgoals, and looking at properly defning permute_bv

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Mar 2010 11:29:54 +0100] rev 1645

One more copy-and-paste in core-haskell.

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

Properly defined permute_bn. No more sorry's in Let strong induction.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Mar 2010 11:10:15 +0100] rev 1643

Showed Let substitution.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Mar 2010 11:01:22 +0100] rev 1642

Only let substitution is left.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Mar 2010 10:44:14 +0100] rev 1641

further in the proof

Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Mar 2010 10:25:33 +0100] rev 1640

trying to prove the string induction for let.

Christian Urban <urbanc@in.tum.de> [Thu, 25 Mar 2010 09:08:42 +0100] rev 1639

added experiemental permute_bn

Christian Urban <urbanc@in.tum.de> [Thu, 25 Mar 2010 08:05:03 +0100] rev 1638

first attempt of strong induction for lets with assignments

Christian Urban <urbanc@in.tum.de> [Thu, 25 Mar 2010 07:21:41 +0100] rev 1637