nominal2: File revisions

Nominal/Ex/Lambda.thy

2011-01-09	Christian Urban	solved subgoals for depth and subst function	file \| diff \| annotate
2011-01-06	Christian Urban	a modified function package where, as a test, True has been injected into the compatibility condictions	file \| diff \| annotate
2011-01-06	Christian Urban	tuned	file \| diff \| annotate
2010-12-31	Christian Urban	changed res keyword to set+ for restrictions; comment by a referee	file \| diff \| annotate
2010-12-28	Christian Urban	automated all strong induction lemmas	file \| diff \| annotate
2010-12-22	Christian Urban	properly exported strong exhaust theorem; cleaned up some examples	file \| diff \| annotate
2010-11-10	Christian Urban	adapted to changes by Florian on the quotient package and removed local fix for function package	file \| diff \| annotate
2010-09-29	Christian Urban	simplified exhaust proofs	file \| diff \| annotate
2010-09-29	Christian Urban	test with induct_schema for simpler strong_ind proofs	file \| diff \| annotate
2010-08-29	Christian Urban	renamed NewParser to Nominal2	file \| diff \| annotate
2010-08-27	Christian Urban	make copies of the "old" files	file \| diff \| annotate
2010-08-26	Christian Urban	"isabelle make test" makes all major examples....they work up to supp theorems (excluding)	file \| diff \| annotate
2010-08-25	Christian Urban	cleaned up (almost completely) the examples	file \| diff \| annotate
2010-08-25	Christian Urban	automatic lifting	file \| diff \| annotate

nominal2