nominal2: Changelog

Christian Urban <urbanc@in.tum.de> [Mon, 07 Feb 2011 15:59:37 +0000] rev 2722

cleaned up the experiments so that the tests go through

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 05 Feb 2011 07:39:00 +0900] rev 2721

merge

Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 05 Feb 2011 07:38:22 +0900] rev 2720

Experiments defining a function on Let

Christian Urban <urbanc@in.tum.de> [Fri, 04 Feb 2011 04:45:04 +0000] rev 2719

updated TODO

Christian Urban <urbanc@in.tum.de> [Fri, 04 Feb 2011 03:52:38 +0000] rev 2718

Lambda.thy which works with Nominal_Isabelle2011

Christian Urban <urbanc@in.tum.de> [Thu, 03 Feb 2011 02:57:04 +0000] rev 2717

merged

Christian Urban <urbanc@in.tum.de> [Thu, 03 Feb 2011 02:51:57 +0000] rev 2716

removed diagnostic code

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 01 Feb 2011 09:07:55 +0900] rev 2715

Only one of the subgoals is needed

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 01 Feb 2011 08:57:50 +0900] rev 2714

Experiments with substitution on set+

Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 01 Feb 2011 08:48:14 +0900] rev 2713

More properties that relate abs_res and abs_set. Also abs_res with less binders.

nominal2