Quot/quotient_tacs.ML
2010-01-27 Christian Urban some slight tuning
2010-01-26 Cezary Kaliszyk Bex1_Bexeq_regular.
2010-01-26 Cezary Kaliszyk Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.
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.
2010-01-26 Cezary Kaliszyk All eq_reflections apart from the one of 'id_apply' can be removed.
2010-01-25 Christian Urban renamed QuotScript to QuotBase
2010-01-21 Cezary Kaliszyk Changed fun_map and rel_map to definitions.
2010-01-21 Cezary Kaliszyk Automatic injection of Bexeq
2010-01-21 Cezary Kaliszyk Automatic cleaning of Bexeq<->Ex1 theorems.
2010-01-21 Cezary Kaliszyk Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles.
2010-01-21 Cezary Kaliszyk Ex1 -> Bex1 Regularization, Preparing Exeq.
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
less more (0) -12 tip