2009-11-27 | Cezary Kaliszyk | Removing arguments of tactics: absrep, rel_refl, reps_same are computed. | file | diff | annotate |
2009-11-27 | Cezary Kaliszyk | More cleaning in QuotMain, identity handling. | file | diff | annotate |
2009-11-27 | Christian Urban | tuned | file | diff | annotate |
2009-11-27 | Christian Urban | some tuning | file | diff | annotate |
2009-11-27 | Christian Urban | simplified gen_frees_tac and properly named abstracted variables | file | diff | annotate |
2009-11-27 | Christian Urban | removed CHANGED' | file | diff | annotate |
2009-11-27 | Christian Urban | introduced a separate lemma for id_simps | file | diff | annotate |
2009-11-27 | Christian Urban | renamed inj_REPABS to inj_repabs_trm | file | diff | annotate |