nominal2: Changelog

Christian Urban <urbanc@in.tum.de> [Wed, 09 Dec 2009 00:03:18 +0100] rev 654

tuned the examples and flagged the problematic cleaning lemmas in FSet

Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 23:32:54 +0100] rev 653

merged

Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 23:30:47 +0100] rev 652

implemented cleaning strategy with fun_map.simps on non-bounded variables; still a few rough edges

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 23:04:40 +0100] rev 651

merge

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 23:04:25 +0100] rev 650

manually cleaned the hard lemma.

Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 22:26:01 +0100] rev 649

merged

Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 22:24:24 +0100] rev 648

decoupled QuotProd from QuotMain and also started new cleaning strategy

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 22:05:01 +0100] rev 647

merge

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 22:03:34 +0100] rev 646

An example which is hard to lift because of the interplay between lambda_prs and unfolding.

Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 22:02:14 +0100] rev 645

proper formulation of all preservation theorems

nominal2