nominal2: File revisions

Nominal/Ex/Let.thy

2010-09-29	Christian Urban	simplified exhaust proofs	file \| diff \| annotate
2010-09-29	Christian Urban	worked example Foo1 with induct_schema	file \| diff \| annotate
2010-09-29	Christian Urban	use also induct_schema for the Let-example (permute_bn is used)	file \| diff \| annotate
2010-09-28	Christian Urban	added Foo1 to explore a contrived example	file \| diff \| annotate
2010-09-27	Christian Urban	added postprocessed fresh-lemmas for constructors	file \| diff \| annotate
2010-09-27	Christian Urban	post-processed eq_iff and supp threormes according to the fv-supp equality	file \| diff \| annotate
2010-09-27	Christian Urban	some experiments	file \| diff \| annotate
2010-08-29	Christian Urban	renamed NewParser to Nominal2	file \| diff \| annotate
2010-08-28	Christian Urban	fiexed problem with constructors that have no arguments	file \| diff \| annotate
2010-08-26	Christian Urban	corrected bug with fv-function generation (that was the problem with recursive binders)	file \| diff \| annotate
2010-08-25	Christian Urban	cleaned up (almost completely) the examples	file \| diff \| annotate \| base

nominal2