isabelle: src/HOL/Lambda/README.html@c81c770f47ef (annotated)

1541 c81c770f47ef Put quotes around URLs in links paulson parents: 1518 diff changeset	1	<HTML><HEAD><TITLE>HOL/Lambda</TITLE></HEAD>
1346 8709e5aaefde New README.html fuile nipkow parents: diff changeset	2	<BODY>
8709e5aaefde New README.html fuile nipkow parents: diff changeset	3
8709e5aaefde New README.html fuile nipkow parents: diff changeset	4	<H1>Lambda Calculus in de Bruijn's Notation</H1>
8709e5aaefde New README.html fuile nipkow parents: diff changeset	5
8709e5aaefde New README.html fuile nipkow parents: diff changeset	6	This theory defines lambda-calculus terms with de Bruijn indixes and proves
8709e5aaefde New README.html fuile nipkow parents: diff changeset	7	confluence of beta, eta and beta+eta.
8709e5aaefde New README.html fuile nipkow parents: diff changeset	8	<P>
1432 2cdb85e5cd90 Minor mod. nipkow parents: 1346 diff changeset	9
1346 8709e5aaefde New README.html fuile nipkow parents: diff changeset	10
1541 c81c770f47ef Put quotes around URLs in links paulson parents: 1518 diff changeset	11	The report
c81c770f47ef Put quotes around URLs in links paulson parents: 1518 diff changeset	12	<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/church-rosser.html">
c81c770f47ef Put quotes around URLs in links paulson parents: 1518 diff changeset	13	More Church-Rosser Proofs (in Isabelle/HOL)</A>
c81c770f47ef Put quotes around URLs in links paulson parents: 1518 diff changeset	14	describes the whole theory.
1346 8709e5aaefde New README.html fuile nipkow parents: diff changeset	15
8709e5aaefde New README.html fuile nipkow parents: diff changeset	16	</BODY>
8709e5aaefde New README.html fuile nipkow parents: diff changeset	17	</HTML>

author	paulson
	Tue, 05 Mar 1996 16:27:01 +0100
changeset 1541	c81c770f47ef
parent 1518	03b770044429
child 1542	03e727af711d
permissions	-rw-r--r--