LFex.thy
2009-12-04 Cezary Kaliszyk Removed previous inj_repabs_tac
2009-12-04 Cezary Kaliszyk rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
2009-12-04 Cezary Kaliszyk Using APPLY_RSP1; again a little bit faster.
2009-12-04 Cezary Kaliszyk The big merge; probably non-functional.
2009-12-04 Cezary Kaliszyk Testing the new tactic everywhere
2009-12-04 Cezary Kaliszyk First version of the deterministic rep-abs-inj-tac.
2009-12-03 Christian Urban removed quot argument...not all examples work anymore
less more (0) -30 -10 -7 tip