IntEx.thy
2009-11-28 Christian Urban removed old inj_repabs_tac; kept only the one with (selective) debugging information
2009-11-28 Christian Urban renamed r_mk_comb_tac to inj_repabs_tac
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 fixed examples in IntEx and FSet
2009-11-28 Christian Urban fixed previous commit
2009-11-28 Christian Urban annotated a proof with all steps and simplified LAMBDA_RES_TAC
2009-11-27 Cezary Kaliszyk Simplifying arguments; got rid of trans2_thm.
less more (0) -30 -10 -8 tip