| Wed, 08 Jun 2011 09:56:39 +0900 | Cezary Kaliszyk | FCB for res binding and simplified proof of subst for type schemes | changeset | files |
| Wed, 08 Jun 2011 07:06:20 +0900 | Cezary Kaliszyk | Simplify ln-trans proof | changeset | files |
| Wed, 08 Jun 2011 07:02:52 +0900 | Cezary Kaliszyk | cbvs can be easily defined without an invariant | changeset | files |
| Tue, 07 Jun 2011 20:58:00 +0100 | Christian Urban | defined the "count-bound-variables-occurences" function which has an accumulator like trans | changeset | files |
| Tue, 07 Jun 2011 17:45:38 +0100 | Christian Urban | merged | changeset | files |
| Tue, 07 Jun 2011 23:42:12 +0900 | Cezary Kaliszyk | remove garbage (proofs that assumes the invariant outside function) | changeset | files |
| Tue, 07 Jun 2011 23:38:39 +0900 | Cezary Kaliszyk | Proof of trans with invariant | changeset | files |