Mon, 15 Nov 2010 01:10:02 +0000 | Christian Urban | fixed bug in fv function where a shallow binder binds lists of names | changeset | files |
Sun, 14 Nov 2010 16:34:47 +0000 | Christian Urban | merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy | changeset | files |
Sun, 14 Nov 2010 12:09:14 +0000 | Christian Urban | deleted special Nominal2_FSet theory | changeset | files |
Sun, 14 Nov 2010 11:46:39 +0000 | Christian Urban | moved rest of the lemmas from Nominal2_FSet to the TypeScheme example | changeset | files |
Sun, 14 Nov 2010 11:05:22 +0000 | Christian Urban | moved most material fron Nominal2_FSet into the Nominal_Base theory | changeset | files |
Sun, 14 Nov 2010 10:02:30 +0000 | Christian Urban | tuned example | changeset | files |
Sun, 14 Nov 2010 01:00:56 +0000 | Christian Urban | lifted permute_bn simp rules | changeset | files |