nominal2: File revisions

Quot/QuotMain.thy

2010-02-10	Cezary Kaliszyk	Some cleaning of proofs.	file \| diff \| annotate
2010-02-10	Cezary Kaliszyk	more minor space and bracket modifications.	file \| diff \| annotate
2010-02-06	Christian Urban	some tuning	file \| diff \| annotate
2010-02-05	Cezary Kaliszyk	A proper version of the attribute	file \| diff \| annotate
2010-01-26	Cezary Kaliszyk	Changed the lambda_prs_simple_conv to use id_apply, now last eq_reflection can be removed from id_simps.	file \| diff \| annotate
2010-01-26	Cezary Kaliszyk	All eq_reflections apart from the one of 'id_apply' can be removed.	file \| diff \| annotate
2010-01-25	Christian Urban	*ids cannot* be object equalities**	file \| diff \| annotate
2010-01-25	Christian Urban	renamed QuotScript to QuotBase	file \| diff \| annotate
2010-01-25	Christian Urban	cleaned some theorems	file \| diff \| annotate
2010-01-21	Cezary Kaliszyk	Automatic injection of Bexeq	file \| diff \| annotate
2010-01-21	Cezary Kaliszyk	Using Bexeq_rsp, and manually lifted lemma with Ex1.	file \| diff \| annotate
2010-01-21	Cezary Kaliszyk	The missing rule.	file \| diff \| annotate
2010-01-16	Christian Urban	liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals	file \| diff \| annotate
2010-01-14	Cezary Kaliszyk	Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.	file \| diff \| annotate

nominal2