nominal2: File revisions

Nominal/Ex/Classical.thy

2011-06-24	Cezary Kaliszyk	Speed-up the completeness proof.	file \| diff \| annotate
2011-06-23	Christian Urban	the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl	file \| diff \| annotate
2011-06-23	Christian Urban	expanded the example	file \| diff \| annotate
2010-12-22	Christian Urban	properly exported strong exhaust theorem; cleaned up some examples	file \| diff \| annotate
2010-08-29	Christian Urban	renamed NewParser to Nominal2	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
2010-06-07	Christian Urban	work on transitivity proof	file \| diff \| annotate
2010-06-02	Christian Urban	fixed problem with bn_info	file \| diff \| annotate
2010-05-12	Christian Urban	fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy	file \| diff \| annotate
2010-05-12	Cezary Kaliszyk	include set_simps and append_simps in fv_rsp	file \| diff \| annotate
2010-05-12	Cezary Kaliszyk	Use equivariance instead of alpha_eqvt	file \| diff \| annotate
2010-05-11	Cezary Kaliszyk	Include raw permutation definitions in eqvt	file \| diff \| annotate
2010-05-11	Cezary Kaliszyk	Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'	file \| diff \| annotate

nominal2