Nominal/Rsp.thy
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.
Mon, 19 Apr 2010 17:26:07 +0200 Christian Urban deleting function perm_arg in favour of the library function mk_perm
Mon, 19 Apr 2010 10:35:08 +0200 Cezary Kaliszyk Accept non-equality eqvt rules in support proofs.
less more (0) -30 -10 -3 tip