| Sun, 29 Nov 2009 08:48:06 +0100 | Cezary Kaliszyk | Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx. | file | diff | annotate |
| Sun, 29 Nov 2009 03:59:18 +0100 | Christian Urban | introduced a global list of respectfulness lemmas; the attribute is [quot_rsp] | file | diff | annotate |
| Sat, 28 Nov 2009 14:45:22 +0100 | Christian Urban | removed old inj_repabs_tac; kept only the one with (selective) debugging information | file | diff | annotate |
| Sat, 28 Nov 2009 14:33:04 +0100 | Christian Urban | renamed r_mk_comb_tac to inj_repabs_tac | file | diff | annotate |
| Sat, 28 Nov 2009 05:43:18 +0100 | Cezary Kaliszyk | Merged and tested that all works. | file | diff | annotate |
| Sat, 28 Nov 2009 05:29:30 +0100 | Cezary Kaliszyk | Finished and tested the new regularize | file | diff | annotate |
| Sat, 28 Nov 2009 04:46:03 +0100 | Christian Urban | fixed examples in IntEx and FSet | file | diff | annotate |