nominal2: Changelog

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 31 May 2011 12:59:10 +0900] rev 2792

Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 31 May 2011 12:54:21 +0900] rev 2791

Simple eqvt proofs with perm_simps for clarity

Christian Urban <urbanc@in.tum.de> [Tue, 31 May 2011 00:36:16 +0100] rev 2790

tuned last commit

Christian Urban <urbanc@in.tum.de> [Tue, 31 May 2011 00:17:22 +0100] rev 2789

functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition

Christian Urban <urbanc@in.tum.de> [Thu, 26 May 2011 06:36:29 +0200] rev 2788

updated to new Isabelle

Christian Urban <urbanc@in.tum.de> [Wed, 25 May 2011 21:38:50 +0200] rev 2787

added eq_iff and distinct lemmas of nominal datatypes to the simplifier

Christian Urban <urbanc@in.tum.de> [Tue, 24 May 2011 19:39:38 +0200] rev 2786