| 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 |