| Mon, 08 Mar 2010 14:31:04 +0100 | Cezary Kaliszyk | Term5 written as nominal_datatype is the recursive let. | file | diff | annotate |
| Mon, 08 Mar 2010 11:10:43 +0100 | Cezary Kaliszyk | Fix permutation addition. | file | diff | annotate |
| Mon, 08 Mar 2010 10:33:55 +0100 | Cezary Kaliszyk | Update the comments | file | diff | annotate |
| Mon, 08 Mar 2010 10:08:31 +0100 | Cezary Kaliszyk | Gather bindings with same binder, and generate only one permutation for them. | file | diff | annotate |
| 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. | file | diff | annotate |
| Thu, 04 Mar 2010 11:16:36 +0100 | Cezary Kaliszyk | A version that just leaves the supp/\supp goal. Obviously not true. | file | diff | annotate |
| Thu, 04 Mar 2010 10:59:52 +0100 | Cezary Kaliszyk | Prove symp and transp of weird without the supp /\ supp = {} assumption. | file | diff | annotate |