Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Nov 2010 16:16:25 +0900] rev 2575
single rename in let2
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Nov 2010 16:14:47 +0900] rev 2574
current isabelle
Christian Urban <urbanc@in.tum.de> [Sun, 21 Nov 2010 02:17:19 +0000] rev 2573
added example Foo2.thy
Christian Urban <urbanc@in.tum.de> [Mon, 15 Nov 2010 20:54:01 +0000] rev 2572
tuned example
Christian Urban <urbanc@in.tum.de> [Mon, 15 Nov 2010 09:52:29 +0000] rev 2571
proved that bn functions return a finite set
Christian Urban <urbanc@in.tum.de> [Mon, 15 Nov 2010 08:17:11 +0000] rev 2570
added a test for the various shallow binders
Christian Urban <urbanc@in.tum.de> [Mon, 15 Nov 2010 01:10:02 +0000] rev 2569
fixed bug in fv function where a shallow binder binds lists of names
Christian Urban <urbanc@in.tum.de> [Sun, 14 Nov 2010 16:34:47 +0000] rev 2568
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de> [Sun, 14 Nov 2010 12:09:14 +0000] rev 2567
deleted special Nominal2_FSet theory
Christian Urban <urbanc@in.tum.de> [Sun, 14 Nov 2010 11:46:39 +0000] rev 2566
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
Christian Urban <urbanc@in.tum.de> [Sun, 14 Nov 2010 11:05:22 +0000] rev 2565
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de> [Sun, 14 Nov 2010 10:02:30 +0000] rev 2564
tuned example
Christian Urban <urbanc@in.tum.de> [Sun, 14 Nov 2010 01:00:56 +0000] rev 2563
lifted permute_bn simp rules
Christian Urban <urbanc@in.tum.de> [Sat, 13 Nov 2010 22:23:26 +0000] rev 2562
lifted permute_bn constants
Christian Urban <urbanc@in.tum.de> [Sat, 13 Nov 2010 10:25:03 +0000] rev 2561
respectfulness for permute_bn functions