| 2010-01-26 | Cezary Kaliszyk | Bex1_Bexeq_regular. | file | diff | annotate |
| 2010-01-26 | Cezary Kaliszyk | Hom Theorem with exists unique | file | diff | annotate |
| 2010-01-26 | Cezary Kaliszyk | 2 cases for regularize with split, lemmas with split now lift. | file | diff | annotate |
| 2010-01-26 | Cezary Kaliszyk | Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work. | file | diff | annotate |
| 2010-01-26 | Cezary Kaliszyk | Sigma cleaning works with split_prs (still manual proof). | file | diff | annotate |
| 2010-01-24 | Christian Urban | test with splits | file | diff | annotate |
| 2010-01-22 | Cezary Kaliszyk | Proper alpha equivalence for Sigma calculus. | file | diff | annotate |
| 2010-01-21 | Cezary Kaliszyk | Lifted Peter's Sigma lemma with Ex1. | file | diff | annotate |
| 2010-01-21 | Cezary Kaliszyk | Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles. | file | diff | annotate |
| 2010-01-20 | Cezary Kaliszyk | Added the Sigma Calculus example | file | diff | annotate |