nominal2: File revisions

Nominal/Nominal2.thy

2011-01-19	Christian Urban	added Minimal file to test things	file \| diff \| annotate
2011-01-17	Christian Urban	exported nominal function code to external file	file \| diff \| annotate
2011-01-07	Christian Urban	derived equivariance for the function graph and function relation	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	removed debugging code abd introduced a guarded tracing function	file \| diff \| annotate
2011-01-06	Christian Urban	cleaned up weakening proof and added a version with finit sets	file \| diff \| annotate
2011-01-06	Christian Urban	made sure the raw datatypes and raw functions do not get any mixfix syntax	file \| diff \| annotate
2011-01-05	Christian Urban	exported the code into a separate file	file \| diff \| annotate
2010-12-31	Christian Urban	changed res keyword to set+ for restrictions; comment by a referee	file \| diff \| annotate
2010-12-31	Christian Urban	added proper case names for all induct and exhaust theorems	file \| diff \| annotate
2010-12-30	Christian Urban	removed local fix for bug in induction_schema; added setup method for strong inductions	file \| diff \| annotate
2010-12-28	Christian Urban	automated all strong induction lemmas	file \| diff \| annotate

nominal2