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

1346 8709e5aaefde New README.html fuile nipkow parents: diff changeset	1	<HTML><HEAD><TITLE>HOL/Lambda/ReadMe</TITLE></HEAD>
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
1518 03b770044429 Moved documentation nipkow parents: 1432 diff changeset	11	A report describing the whole theory is found here:<br>
03b770044429 Moved documentation nipkow parents: 1432 diff changeset	12	<A HREF=http://www4.informatik.tu-muenchen.de/~nipkow/pubs/church-rosser.html>
03b770044429 Moved documentation nipkow parents: 1432 diff changeset	13	More Church-Rosser Proofs (in Isabelle/HOL)</A>.
1346 8709e5aaefde New README.html fuile nipkow parents: diff changeset	14
8709e5aaefde New README.html fuile nipkow parents: diff changeset	15	</BODY>
8709e5aaefde New README.html fuile nipkow parents: diff changeset	16	</HTML>

author	nipkow
	Thu, 22 Feb 1996 18:25:19 +0100
changeset 1518	03b770044429
parent 1432	2cdb85e5cd90
child 1541	c81c770f47ef
permissions	-rw-r--r--