Nominal/Ex/Lambda.thy
2011-01-09 Christian Urban solved subgoals for depth and subst function
2011-01-06 Christian Urban a modified function package where, as a test, True has been injected into the compatibility condictions
2011-01-06 Christian Urban tuned
2010-12-31 Christian Urban changed res keyword to set+ for restrictions; comment by a referee
2010-12-28 Christian Urban automated all strong induction lemmas
2010-12-22 Christian Urban properly exported strong exhaust theorem; cleaned up some examples
less more (0) -30 -10 -6 tip