| Mon, 08 Mar 2010 10:33:55 +0100 | Cezary Kaliszyk | Update the comments | changeset | files |
| Mon, 08 Mar 2010 10:08:31 +0100 | Cezary Kaliszyk | Gather bindings with same binder, and generate only one permutation for them. | changeset | files |
| Mon, 08 Mar 2010 02:40:16 +0100 | Cezary Kaliszyk | Undo effects of simp. | changeset | files |
| Sun, 07 Mar 2010 21:30:57 +0100 | Christian Urban | merged | changeset | files |
| Sun, 07 Mar 2010 21:30:12 +0100 | Christian Urban | updated to renamings in Isabelle | changeset | files |
| Thu, 04 Mar 2010 15:56:58 +0100 | Christian Urban | merged | changeset | files |
| Thu, 04 Mar 2010 15:31:34 +0100 | Christian Urban | merged | changeset | files |
| Thu, 04 Mar 2010 15:31:21 +0100 | Christian Urban | more proofs in Abs and work on Core Haskell | changeset | files |
| Wed, 03 Mar 2010 19:10:40 +0100 | Christian Urban | added a lemma that permutations can be represented as sums of swapping | changeset | files |
| Fri, 05 Mar 2010 18:14:04 +0100 | Cezary Kaliszyk | Still unable to show supp=fv for let with one existential. | changeset | files |
| Fri, 05 Mar 2010 17:09:48 +0100 | Cezary Kaliszyk | Ported LF to the parser interface. | changeset | files |
| Fri, 05 Mar 2010 14:56:19 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Fri, 05 Mar 2010 14:55:21 +0100 | Cezary Kaliszyk | Lift fv and bn eqvts; no need to lift alpha_eqvt. | changeset | files |
| Fri, 05 Mar 2010 13:04:47 +0100 | Cezary Kaliszyk | Not much progress about the single existential let case. | changeset | files |
| Fri, 05 Mar 2010 10:23:40 +0100 | Cezary Kaliszyk | Fixed LF for one quantifier over 2 premises. | changeset | files |