nominal2: File revisions

Quot/quotient_tacs.ML

2010-01-27	Christian Urban	some slight tuning	file \| diff \| annotate
2010-01-26	Cezary Kaliszyk	Bex1_Bexeq_regular.	file \| diff \| annotate
2010-01-26	Cezary Kaliszyk	Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.	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	renamed QuotScript to QuotBase	file \| diff \| annotate
2010-01-21	Cezary Kaliszyk	Changed fun_map and rel_map to definitions.	file \| diff \| annotate
2010-01-21	Cezary Kaliszyk	Automatic injection of Bexeq	file \| diff \| annotate
2010-01-21	Cezary Kaliszyk	Automatic cleaning of Bexeq<->Ex1 theorems.	file \| diff \| annotate
2010-01-21	Cezary Kaliszyk	Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles.	file \| diff \| annotate
2010-01-21	Cezary Kaliszyk	Ex1 -> Bex1 Regularization, Preparing Exeq.	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

nominal2