| changeset 21138 | afdd72fc6c4f |
| parent 21101 | 286d68ce3f5b |
| child 21143 | 56695d1f45cf |
| 21137:8a1d62375ff8 | 21138:afdd72fc6c4f |
|---|---|
1 (* $Id$ *) |
1 (* $Id$ *) |
2 |
2 |
3 theory CR |
3 theory CR |
4 imports Lam_substs |
4 imports Lam_Funs |
5 begin |
5 begin |
6 |
6 |
7 text {* The Church-Rosser proof from Barendregt's book *} |
7 text {* The Church-Rosser proof from Barendregt's book *} |
8 |
8 |
9 lemma forget: |
9 lemma forget: |