Nominal/Parser.thy
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
Tue, 02 Mar 2010 21:43:27 +0100 Cezary Kaliszyk Comment out the part that does not work with 2 quantifiers.
Tue, 02 Mar 2010 17:48:41 +0100 Cezary Kaliszyk Porting from Lift to Parser; until defining the Quotient type.
less more (0) -10 -7 tip