Nominal/Parser.thy
Fri, 05 Mar 2010 14:55:21 +0100 Cezary Kaliszyk Lift fv and bn eqvts; no need to lift alpha_eqvt.
Thu, 04 Mar 2010 18:57:23 +0100 Cezary Kaliszyk Lift distinct.
Thu, 04 Mar 2010 15:55:53 +0100 Cezary Kaliszyk Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Thu, 04 Mar 2010 15:15:44 +0100 Cezary Kaliszyk Lift BV,FV,Permutations and injection :).
Thu, 04 Mar 2010 12:00:11 +0100 Cezary Kaliszyk Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Wed, 03 Mar 2010 14:22:58 +0100 Cezary Kaliszyk Fix eqvt for multiple quantifiers.
Wed, 03 Mar 2010 11:42:15 +0100 Cezary Kaliszyk weird eqvt
less more (0) -10 -7 tip