nominal2: File revisions

Nominal/Nominal2_Base.thy

2010-12-19	Christian Urban	a stronger statement for at_set_avoiding	file \| diff \| annotate
2010-12-16	Christian Urban	simple cases for strong inducts done; infrastructure for the difficult ones is there	file \| diff \| annotate
2010-12-14	Christian Urban	freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)	file \| diff \| annotate
2010-12-07	Christian Urban	moved general theorems into the libraries	file \| diff \| annotate
2010-11-29	Christian Urban	isarfied some of the high-level proofs	file \| diff \| annotate
2010-11-29	Christian Urban	completed proofs in Foo2	file \| diff \| annotate
2010-11-28	Christian Urban	completed the strong exhausts rules for Foo2 using general lemmas	file \| diff \| annotate
2010-11-27	Christian Urban	tuned proof to reduce number of warnings	file \| diff \| annotate
2010-11-27	Christian Urban	disabled the Foo examples, because of heavy work	file \| diff \| annotate
2010-11-21	Christian Urban	added example Foo2.thy	file \| diff \| annotate
2010-11-14	Christian Urban	merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy	file \| diff \| annotate \| base
2010-03-20	Christian Urban	moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas	file \| diff \| annotate
2010-03-02	Christian Urban	updated (added lemma about commuting permutations)	file \| diff \| annotate
2010-02-25	Christian Urban	moved Nominal to "toplevel"	file \| diff \| annotate \| base

nominal2