| Wed, 03 Feb 2010 12:11:23 +0100 | Cezary Kaliszyk | The alpha-equivalence relation for let-rec. Not sure if correct... | file | diff | annotate |
| Tue, 02 Feb 2010 13:10:46 +0100 | Cezary Kaliszyk | LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left. | file | diff | annotate |
| Tue, 02 Feb 2010 10:43:48 +0100 | Cezary Kaliszyk | With induct instead of induct_tac, just one induction is sufficient. | file | diff | annotate |
| Tue, 02 Feb 2010 10:20:54 +0100 | Cezary Kaliszyk | General alpha_gen_trans for one-variable abstraction. | file | diff | annotate |
| Mon, 01 Feb 2010 11:39:59 +0100 | Cezary Kaliszyk | The current state of fv vs supp proofs in LF. | file | diff | annotate |
| Mon, 01 Feb 2010 11:16:13 +0100 | Cezary Kaliszyk | More proofs in the LF example. | file | diff | annotate |