2010-02-08 | Christian Urban | moved some lemmas to Nominal; updated all files | file | diff | annotate |
2010-02-02 | Cezary Kaliszyk | First experiments in Terms. | file | diff | annotate |
2010-02-02 | Cezary Kaliszyk | Disambiguating the syntax. | file | diff | annotate |
2010-02-02 | Cezary Kaliszyk | Minor uncommited changes from LamEx2. | file | diff | annotate |
2010-02-02 | Cezary Kaliszyk | Some equivariance machinery that comes useful in LF. | file | diff | annotate |
2010-02-02 | Cezary Kaliszyk | Generalized the eqvt proof for single binders. | file | diff | annotate |
2010-02-02 | Cezary Kaliszyk | General alpha_gen_trans for one-variable abstraction. | file | diff | annotate |
2010-02-02 | Cezary Kaliszyk | With unfolding Rep/Abs_eqvt no longer needed. | file | diff | annotate |
2010-02-02 | Cezary Kaliszyk | Lam2 finished apart from Rep_eqvt. | file | diff | annotate |
2010-02-01 | Cezary Kaliszyk | All should be ok now. | file | diff | annotate |
2010-02-01 | Cezary Kaliszyk | Fixed wrong rename. | file | diff | annotate |