| changeset 13360 | ece4b151f963 |
| parent 8888 | 343c304e714a |
| child 15283 | f21466450330 |
| 13359:982827aacb39 | 13360:ece4b151f963 |
|---|---|
8 confluence of beta, eta and beta+eta. |
8 confluence of beta, eta and beta+eta. |
9 <P> |
9 <P> |
10 |
10 |
11 |
11 |
12 The paper |
12 The paper |
13 <A HREF="http://www.in.tum.de/~nipkow/pubs/jar2000.html"> |
13 <A HREF="http://www.in.tum.de/~nipkow/pubs/jar2001.html"> |
14 More Church-Rosser Proofs (in Isabelle/HOL)</A> |
14 More Church-Rosser Proofs (in Isabelle/HOL)</A> |
15 describes the whole theory. |
15 describes the whole theory. |
16 |
16 |
17 <HR> |
17 <HR> |
18 |
18 |