Mon, 03 May 2010 15:37:21 +0200 | Cezary Kaliszyk | alpha_eqvt_tac fixed to work when the existential is not at the top level. | file | diff | annotate |
Mon, 19 Apr 2010 17:26:07 +0200 | Christian Urban | deleting function perm_arg in favour of the library function mk_perm | file | diff | annotate |
Mon, 19 Apr 2010 10:35:08 +0200 | Cezary Kaliszyk | Accept non-equality eqvt rules in support proofs. | file | diff | annotate |