Nominal/LFex.thy
Mon, 08 Mar 2010 11:12:15 +0100 Cezary Kaliszyk More fine-grained nominal restriction for debugging.
Fri, 05 Mar 2010 17:09:48 +0100 Cezary Kaliszyk Ported LF to the parser interface.
Fri, 05 Mar 2010 10:23:40 +0100 Cezary Kaliszyk Fixed LF for one quantifier over 2 premises.
Tue, 02 Mar 2010 15:12:50 +0100 Cezary Kaliszyk Minor
Tue, 02 Mar 2010 11:04:49 +0100 Cezary Kaliszyk Fixed eqvt code.
Fri, 26 Feb 2010 15:42:00 +0100 Cezary Kaliszyk RSP of perms can be shown in one go.
Fri, 26 Feb 2010 15:10:55 +0100 Cezary Kaliszyk Change in signature of prove_const_rsp for general lifting.
Fri, 26 Feb 2010 13:57:43 +0100 Cezary Kaliszyk Permutation and FV_Alpha interface change.
Thu, 25 Feb 2010 12:15:11 +0100 Cezary Kaliszyk Code for proving eqvt, still in Terms.
Thu, 25 Feb 2010 07:48:57 +0100 Christian Urban merged
Thu, 25 Feb 2010 07:48:33 +0100 Christian Urban moved Nominal to "toplevel"
less more (0) tip