QuotMain.thy
2009-11-28 Christian Urban further proper merge
2009-11-28 Christian Urban merged
2009-11-28 Christian Urban more simplification
2009-11-28 Cezary Kaliszyk Merged and tested that all works.
2009-11-28 Cezary Kaliszyk Finished and tested the new regularize
2009-11-28 Christian Urban more tuning of the repabs-tactics
2009-11-28 Christian Urban merged
2009-11-28 Christian Urban fixed previous commit
2009-11-28 Cezary Kaliszyk Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
2009-11-28 Cezary Kaliszyk Merged comment
2009-11-28 Christian Urban some slight tuning of the apply-tactic
2009-11-28 Christian Urban annotated a proof with all steps and simplified LAMBDA_RES_TAC
2009-11-27 Christian Urban replaced FIRST' (map rtac list) with resolve_tac list
2009-11-27 Cezary Kaliszyk Simplifying arguments; got rid of trans2_thm.
2009-11-27 Cezary Kaliszyk Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
2009-11-27 Cezary Kaliszyk More cleaning in QuotMain, identity handling.
less more (0) -300 -100 -16 tip