Nominal/Ex/Lambda.thy
Thu, 06 Jan 2011 23:06:45 +0000 Christian Urban a modified function package where, as a test, True has been injected into the compatibility condictions
Thu, 06 Jan 2011 14:02:10 +0000 Christian Urban tuned
Fri, 31 Dec 2010 15:37:04 +0000 Christian Urban changed res keyword to set+ for restrictions; comment by a referee
Tue, 28 Dec 2010 19:51:25 +0000 Christian Urban automated all strong induction lemmas
Wed, 22 Dec 2010 09:13:25 +0000 Christian Urban properly exported strong exhaust theorem; cleaned up some examples
Wed, 10 Nov 2010 13:46:21 +0000 Christian Urban adapted to changes by Florian on the quotient package and removed local fix for function package
less more (0) -30 -10 -6 tip