nominal2: Changelog

Christian Urban <urbanc@in.tum.de> [Fri, 03 Sep 2010 22:35:35 +0800] rev 2465

adapted paper to changes

Christian Urban <urbanc@in.tum.de> [Fri, 03 Sep 2010 22:22:43 +0800] rev 2464

made the fv-definition aggree more with alpha (needed in the support proofs)

Christian Urban <urbanc@in.tum.de> [Fri, 03 Sep 2010 20:53:09 +0800] rev 2463

removed lemma finite_set (already in simpset)

Christian Urban <urbanc@in.tum.de> [Fri, 03 Sep 2010 20:48:45 +0800] rev 2462

added supp_set lemma

Christian Urban <urbanc@in.tum.de> [Thu, 02 Sep 2010 18:10:06 +0800] rev 2461

some experiments with support

Christian Urban <urbanc@in.tum.de> [Thu, 02 Sep 2010 01:16:26 +0800] rev 2460

added eqvt-attribute for permute_abs lemmas

Christian Urban <urbanc@in.tum.de> [Tue, 31 Aug 2010 21:03:08 +0800] rev 2459

slides of my talk

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 30 Aug 2010 15:59:50 +0900] rev 2458

merge

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 30 Aug 2010 15:59:16 +0900] rev 2457

update qpaper to new isabelle

Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 30 Aug 2010 15:55:08 +0900] rev 2456

No need to unfold mem_def with rsp/prs (requires new isabelle).

nominal2