nominal2: File revisions

Nominal/nominal_library.ML

Thu, 06 Jan 2011 19:57:57 +0000	Christian Urban	removed debugging code abd introduced a guarded tracing function	file \| diff \| annotate
Tue, 04 Jan 2011 13:47:38 +0000	Christian Urban	final version of the ESOP paper; used set+ instead of res as requested by one reviewer	file \| diff \| annotate
Mon, 03 Jan 2011 16:19:27 +0000	Christian Urban	simple cases for string rule inductions	file \| diff \| annotate
Tue, 28 Dec 2010 19:51:25 +0000	Christian Urban	automated all strong induction lemmas	file \| diff \| annotate
Thu, 23 Dec 2010 00:22:41 +0000	Christian Urban	moved generic functions into nominal_library	file \| diff \| annotate
Wed, 22 Dec 2010 12:47:09 +0000	Christian Urban	updated to Isabelle 22 December	file \| diff \| annotate
Wed, 22 Dec 2010 12:17:49 +0000	Christian Urban	a bit tuning	file \| diff \| annotate
Tue, 21 Dec 2010 10:28:08 +0000	Christian Urban	all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code	file \| diff \| annotate

nominal2