equal
deleted
inserted
replaced
7 This theory defines lambda-calculus terms with de Bruijn indixes and proves |
7 This theory defines lambda-calculus terms with de Bruijn indixes and proves |
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 report |
12 The paper |
13 <A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/church-rosser.html"> |
13 <A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/cade96.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 |
19 <P>Last modified 5 March 1996 |
19 <P>Last modified 4 April 1996 |
20 |
20 |
21 </BODY> |
21 </BODY> |
22 </HTML> |
22 </HTML> |