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

15283 f21466450330 DOCTYPE declaration added webertj parents: 13360 diff changeset	1	<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
f21466450330 DOCTYPE declaration added webertj parents: 13360 diff changeset	2
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	3	<HTML>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	4
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	5	<HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	6	<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	7	<TITLE>HOL/Lambda</TITLE>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	8	</HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	9
1346 8709e5aaefde New README.html fuile nipkow parents: diff changeset	10	<BODY>
8709e5aaefde New README.html fuile nipkow parents: diff changeset	11
8709e5aaefde New README.html fuile nipkow parents: diff changeset	12	<H1>Lambda Calculus in de Bruijn's Notation</H1>
8709e5aaefde New README.html fuile nipkow parents: diff changeset	13
8709e5aaefde New README.html fuile nipkow parents: diff changeset	14	This theory defines lambda-calculus terms with de Bruijn indixes and proves
8709e5aaefde New README.html fuile nipkow parents: diff changeset	15	confluence of beta, eta and beta+eta.
8709e5aaefde New README.html fuile nipkow parents: diff changeset	16	<P>
1432 2cdb85e5cd90 Minor mod. nipkow parents: 1346 diff changeset	17
1346 8709e5aaefde New README.html fuile nipkow parents: diff changeset	18
1645 be85d119a805 Moved link to paper. nipkow parents: 1542 diff changeset	19	The paper
13360 ece4b151f963 * empty log message * nipkow parents: 8888 diff changeset	20	<A HREF="http://www.in.tum.de/~nipkow/pubs/jar2001.html">
1541 c81c770f47ef Put quotes around URLs in links paulson parents: 1518 diff changeset	21	More Church-Rosser Proofs (in Isabelle/HOL)</A>
c81c770f47ef Put quotes around URLs in links paulson parents: 1518 diff changeset	22	describes the whole theory.
1346 8709e5aaefde New README.html fuile nipkow parents: diff changeset	23
1542 03e727af711d Put quotes around URLs in links paulson parents: 1541 diff changeset	24	<HR>
03e727af711d Put quotes around URLs in links paulson parents: 1541 diff changeset	25
8888 343c304e714a fixed link nipkow parents: 2162 diff changeset	26	<P>Last modified 20.5.2000
1542 03e727af711d Put quotes around URLs in links paulson parents: 1541 diff changeset	27
1346 8709e5aaefde New README.html fuile nipkow parents: diff changeset	28	</BODY>
8709e5aaefde New README.html fuile nipkow parents: diff changeset	29	</HTML>

author	wenzelm
	Wed, 12 May 2010 14:17:26 +0200
changeset 36862	952b2b102a0a
parent 15582	7219facb3fd0
permissions	-rw-r--r--