HTML 4.01 Transitional conformity
authorwebertj
Mon Mar 07 19:17:07 2005 +0100 (2005-03-07)
changeset 155827219facb3fd0
parent 15581 f07e865d9d40
child 15583 256c5e6b314f
HTML 4.01 Transitional conformity
README.html
src/CTT/README.html
src/Cube/README.html
src/FOL/README.html
src/HOL/Algebra/README.html
src/HOL/Auth/Guard/README.html
src/HOL/Auth/README.html
src/HOL/AxClasses/README.html
src/HOL/Complex/README.html
src/HOL/Hoare/README.html
src/HOL/IMPP/README.html
src/HOL/IOA/README.html
src/HOL/Induct/README.html
src/HOL/Isar_examples/README.html
src/HOL/Lambda/README.html
src/HOL/Library/README.html
src/HOL/Modelcheck/README.html
src/HOL/Prolog/README.html
src/HOL/README.html
src/HOL/Real/HahnBanach/README.html
src/HOL/TLA/README.html
src/HOL/UNITY/Comp/README.html
src/HOL/UNITY/README.html
src/HOL/UNITY/Simple/README.html
src/HOL/W0/README.html
src/HOL/ex/README.html
src/HOLCF/FOCUS/README.html
src/HOLCF/IMP/README.html
src/HOLCF/IOA/README.html
src/HOLCF/README.html
src/LCF/README.html
src/Sequents/README.html
src/ZF/AC/README.html
src/ZF/Coind/README.html
src/ZF/Constructible/README.html
src/ZF/IMP/README.html
src/ZF/README.html
src/ZF/Resid/README.html
src/ZF/ex/README.html
     1.1 --- a/README.html	Mon Mar 07 18:40:36 2005 +0100
     1.2 +++ b/README.html	Mon Mar 07 19:17:07 2005 +0100
     1.3 @@ -1,9 +1,9 @@
     1.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     1.5  
     1.6 +<!-- $Id$ -->
     1.7 +
     1.8  <html>
     1.9  
    1.10 -<!-- $Id$ -->
    1.11 -
    1.12  <head>
    1.13    <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
    1.14    <title>The Isabelle System Distribution</title>
     2.1 --- a/src/CTT/README.html	Mon Mar 07 18:40:36 2005 +0100
     2.2 +++ b/src/CTT/README.html	Mon Mar 07 19:17:07 2005 +0100
     2.3 @@ -1,6 +1,15 @@
     2.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2.5  
     2.6 -<HTML><HEAD><TITLE>CTT/README</TITLE></HEAD><BODY>
     2.7 +<!-- $Id$ -->
     2.8 +
     2.9 +<HTML>
    2.10 +
    2.11 +<HEAD>
    2.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
    2.13 +  <TITLE>CTT/README</TITLE>
    2.14 +</HEAD>
    2.15 +
    2.16 +<BODY>
    2.17  
    2.18  <H2>CTT: Constructive Type Theory</H2>
    2.19  
     3.1 --- a/src/Cube/README.html	Mon Mar 07 18:40:36 2005 +0100
     3.2 +++ b/src/Cube/README.html	Mon Mar 07 19:17:07 2005 +0100
     3.3 @@ -1,6 +1,15 @@
     3.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     3.5  
     3.6 -<HTML><HEAD><TITLE>Cube/README</TITLE></HEAD><BODY>
     3.7 +<!-- $Id$ -->
     3.8 +
     3.9 +<HTML>
    3.10 +
    3.11 +<HEAD>
    3.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
    3.13 +  <TITLE>Cube/README</TITLE>
    3.14 +</HEAD>
    3.15 +
    3.16 +<BODY>
    3.17  
    3.18  <H2>Cube: Barendregt's Lambda-Cube</H2>
    3.19  
     4.1 --- a/src/FOL/README.html	Mon Mar 07 18:40:36 2005 +0100
     4.2 +++ b/src/FOL/README.html	Mon Mar 07 19:17:07 2005 +0100
     4.3 @@ -1,6 +1,15 @@
     4.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     4.5  
     4.6 -<html><head><title>FOL/README</title></head><body>
     4.7 +<!-- $Id$ -->
     4.8 +
     4.9 +<html>
    4.10 +
    4.11 +<head>
    4.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
    4.13 +  <title>FOL/README</title>
    4.14 +</head>
    4.15 +
    4.16 +<body>
    4.17  
    4.18  <h2>FOL: First-Order Logic with Natural Deduction</h2>
    4.19  
    4.20 @@ -19,4 +28,5 @@
    4.21  <li>Antony Galton, Logic for Information Technology (Wiley, 1990)
    4.22  <li>Michael Dummett, Elements of Intuitionism (Oxford, 1977)
    4.23  </ul>
    4.24 -</body></html>
    4.25 +</body>
    4.26 +</html>
     5.1 --- a/src/HOL/Algebra/README.html	Mon Mar 07 18:40:36 2005 +0100
     5.2 +++ b/src/HOL/Algebra/README.html	Mon Mar 07 19:17:07 2005 +0100
     5.3 @@ -1,7 +1,15 @@
     5.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     5.5  
     5.6  <!-- $Id$ -->
     5.7 -<HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>
     5.8 +
     5.9 +<HTML>
    5.10 +
    5.11 +<HEAD>
    5.12 +  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
    5.13 +  <TITLE>HOL/Algebra/README.html</TITLE>
    5.14 +</HEAD>
    5.15 +
    5.16 +<BODY>
    5.17  
    5.18  <H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1>
    5.19  
    5.20 @@ -110,4 +118,5 @@
    5.21  <ADDRESS>
    5.22  <P><A HREF="http://www4.in.tum.de/~ballarin">Clemens Ballarin</A>.
    5.23  </ADDRESS>
    5.24 -</BODY></HTML>
    5.25 +</BODY>
    5.26 +</HTML>
     6.1 --- a/src/HOL/Auth/Guard/README.html	Mon Mar 07 18:40:36 2005 +0100
     6.2 +++ b/src/HOL/Auth/Guard/README.html	Mon Mar 07 19:17:07 2005 +0100
     6.3 @@ -1,7 +1,15 @@
     6.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     6.5  
     6.6  <!-- $Id$ -->
     6.7 -<HTML><HEAD><TITLE>HOL/Auth/Guard/README.html</TITLE></HEAD><BODY>
     6.8 +
     6.9 +<HTML>
    6.10 +
    6.11 +<HEAD>
    6.12 +  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
    6.13 +  <TITLE>HOL/Auth/Guard/README.html</TITLE>
    6.14 +</HEAD>
    6.15 +
    6.16 +<BODY>
    6.17  
    6.18  <H1>Protocol-Independent Secrecy Results</H1>
    6.19  
    6.20 @@ -58,4 +66,5 @@
    6.21  <A HREF="http://www.lri.fr/~blanqui/">Frederic Blanqui</A>,
    6.22  <A HREF="mailto:blanqui@lri.fr">blanqui@lri.fr</A>
    6.23  </ADDRESS>
    6.24 -</BODY></HTML>
    6.25 +</BODY>
    6.26 +</HTML>
     7.1 --- a/src/HOL/Auth/README.html	Mon Mar 07 18:40:36 2005 +0100
     7.2 +++ b/src/HOL/Auth/README.html	Mon Mar 07 19:17:07 2005 +0100
     7.3 @@ -1,6 +1,15 @@
     7.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     7.5  
     7.6 -<HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
     7.7 +<!-- $Id$ -->
     7.8 +
     7.9 +<HTML>
    7.10 +
    7.11 +<HEAD>
    7.12 +  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
    7.13 +  <TITLE>HOL/Auth/README</TITLE>
    7.14 +</HEAD>
    7.15 +
    7.16 +<BODY>
    7.17  
    7.18  <H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
    7.19  
    7.20 @@ -45,4 +54,5 @@
    7.21  HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
    7.22  <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    7.23  </ADDRESS>
    7.24 -</BODY></HTML>
    7.25 +</BODY>
    7.26 +</HTML>
     8.1 --- a/src/HOL/AxClasses/README.html	Mon Mar 07 18:40:36 2005 +0100
     8.2 +++ b/src/HOL/AxClasses/README.html	Mon Mar 07 19:17:07 2005 +0100
     8.3 @@ -1,10 +1,12 @@
     8.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     8.5  
     8.6  <!-- $Id$ -->
     8.7 +
     8.8  <html>
     8.9  
    8.10  <head>
    8.11 -<title>HOL/AxClasses</title>
    8.12 +  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
    8.13 +  <title>HOL/AxClasses</title>
    8.14  </head>
    8.15  
    8.16  <body>
    8.17 @@ -14,6 +16,5 @@
    8.18  href="http://isabelle.in.tum.de/doc/axclass.pdf">Using Axiomatic Type
    8.19  Classes in Isabelle</a>.  See also FOL/ex/NatClass for the natural
    8.20  number example.
    8.21 -
    8.22  </body>
    8.23  </html>
     9.1 --- a/src/HOL/Complex/README.html	Mon Mar 07 18:40:36 2005 +0100
     9.2 +++ b/src/HOL/Complex/README.html	Mon Mar 07 19:17:07 2005 +0100
     9.3 @@ -1,8 +1,15 @@
     9.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     9.5  
     9.6 -<HTML><HEAD><TITLE>HOL/Complex/README</TITLE>
     9.7 -		<meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
     9.8 -	</HEAD><BODY>
     9.9 +<!-- $Id$ -->
    9.10 +
    9.11 +<HTML>
    9.12 +
    9.13 +<HEAD>
    9.14 +  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
    9.15 +  <TITLE>HOL/Complex/README</TITLE>
    9.16 +</HEAD>
    9.17 +
    9.18 +<BODY>
    9.19  
    9.20  <H1>Complex: The Complex Numbers</H1>
    9.21  		<P>This directory defines the type <KBD>complex</KBD> of the complex numbers,
    9.22 @@ -56,5 +63,5 @@
    9.23  </ul>
    9.24  <HR>
    9.25  <P>Last modified $Date$
    9.26 -
    9.27 +</BODY>
    9.28  </HTML>
    10.1 --- a/src/HOL/Hoare/README.html	Mon Mar 07 18:40:36 2005 +0100
    10.2 +++ b/src/HOL/Hoare/README.html	Mon Mar 07 19:17:07 2005 +0100
    10.3 @@ -1,6 +1,15 @@
    10.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    10.5  
    10.6 -<HTML><HEAD><TITLE>HOL/Hoare/ReadMe</TITLE></HEAD><BODY>
    10.7 +<!-- $Id$ -->
    10.8 +
    10.9 +<HTML>
   10.10 +
   10.11 +<HEAD>
   10.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   10.13 +  <TITLE>HOL/Hoare/ReadMe</TITLE>
   10.14 +</HEAD>
   10.15 +
   10.16 +<BODY>
   10.17  
   10.18  <H2>Hoare Logic for a Simple WHILE Language</H2>
   10.19  
   10.20 @@ -83,4 +92,5 @@
   10.21  <P>
   10.22  and the embeding is deep, i.e. there is a concrete datatype of programs. The
   10.23  latter is not really necessary.
   10.24 -</BODY></HTML>
   10.25 +</BODY>
   10.26 +</HTML>
    11.1 --- a/src/HOL/IMPP/README.html	Mon Mar 07 18:40:36 2005 +0100
    11.2 +++ b/src/HOL/IMPP/README.html	Mon Mar 07 19:17:07 2005 +0100
    11.3 @@ -1,9 +1,15 @@
    11.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    11.5  
    11.6  <!-- $Id$ -->
    11.7 -<HTML><HEAD>
    11.8 -<TITLE>HOL/IMPP/README</TITLE>
    11.9 -</HEAD><BODY>
   11.10 +
   11.11 +<HTML>
   11.12 +
   11.13 +<HEAD>
   11.14 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   11.15 +  <TITLE>HOL/IMPP/README</TITLE>
   11.16 +</HEAD>
   11.17 +
   11.18 +<BODY>
   11.19  
   11.20  <H2>IMPP--An imperative language with procedures</H2>
   11.21  
    12.1 --- a/src/HOL/IOA/README.html	Mon Mar 07 18:40:36 2005 +0100
    12.2 +++ b/src/HOL/IOA/README.html	Mon Mar 07 19:17:07 2005 +0100
    12.3 @@ -1,18 +1,27 @@
    12.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    12.5  
    12.6 -<HTML><HEAD><TITLE>HOLCF/IOA/README</TITLE></HEAD><BODY>
    12.7 +<!-- $Id -->
    12.8 +
    12.9 +<html>
   12.10 +
   12.11 +<head>
   12.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   12.13 +  <title>HOLCF/IOA/README</title>
   12.14 +</head>
   12.15  
   12.16 -<H3>IOA: A basic formalization of I/O automata in HOL</H3>
   12.17 +<body>
   12.18 +
   12.19 +<h3>IOA: A basic formalization of I/O automata in HOL</h3>
   12.20  
   12.21 -Author:     Konrad Slind, Tobias Nipkow and Olaf M&uuml;ller<BR>
   12.22 -Copyright   1995,1996 Technische Universit&auml;t M&uuml;nchen<P>
   12.23 +Author:     Konrad Slind, Tobias Nipkow and Olaf M&uuml;ller<br>
   12.24 +Copyright   1995,1996 Technische Universit&auml;t M&uuml;nchen
   12.25 +
   12.26 +<p>
   12.27  
   12.28  This directory contains a formalization of the meta theory of I/O automata in HOL.
   12.29 -This formalization has been significantly changed and extended. The new version is available in the subdirectory HOLCF/IOA. There are also the proofs of two communication protocols which formerly
   12.30 -have been here. 
   12.31 -
   12.32 +This formalization has been significantly changed and extended.  The new version
   12.33 +is available in the subdirectory HOLCF/IOA.  There are also the proofs of two
   12.34 +communication protocols which formerly have been here.
   12.35  
   12.36 -</BODY></HTML>
   12.37 -
   12.38 -
   12.39 -
   12.40 +</body>
   12.41 +</html>
    13.1 --- a/src/HOL/Induct/README.html	Mon Mar 07 18:40:36 2005 +0100
    13.2 +++ b/src/HOL/Induct/README.html	Mon Mar 07 19:17:07 2005 +0100
    13.3 @@ -1,7 +1,15 @@
    13.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    13.5  
    13.6  <!-- $Id$ -->
    13.7 -<HTML><HEAD><TITLE>HOL/Induct/README</TITLE></HEAD><BODY>
    13.8 +
    13.9 +<HTML>
   13.10 +
   13.11 +<HEAD>
   13.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   13.13 +  <TITLE>HOL/Induct/README</TITLE>
   13.14 +</HEAD>
   13.15 +
   13.16 +<BODY>
   13.17  
   13.18  <H2>Induct--Examples of (Co)Inductive Definitions</H2>
   13.19  
    14.1 --- a/src/HOL/Isar_examples/README.html	Mon Mar 07 18:40:36 2005 +0100
    14.2 +++ b/src/HOL/Isar_examples/README.html	Mon Mar 07 19:17:07 2005 +0100
    14.3 @@ -1,10 +1,12 @@
    14.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    14.5  
    14.6  <!-- $Id$ -->
    14.7 +
    14.8  <html>
    14.9  
   14.10  <head>
   14.11 -<title>HOL/Isar_examples</title>
   14.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   14.13 +  <title>HOL/Isar_examples</title>
   14.14  </head>
   14.15  
   14.16  <body>
   14.17 @@ -15,6 +17,5 @@
   14.18  also the included document, or the <a
   14.19  href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar page</a> for more
   14.20  information.
   14.21 -
   14.22  </body>
   14.23  </html>
    15.1 --- a/src/HOL/Lambda/README.html	Mon Mar 07 18:40:36 2005 +0100
    15.2 +++ b/src/HOL/Lambda/README.html	Mon Mar 07 19:17:07 2005 +0100
    15.3 @@ -1,7 +1,14 @@
    15.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    15.5  
    15.6  <!-- $Id$ -->
    15.7 -<HTML><HEAD><TITLE>HOL/Lambda</TITLE></HEAD>
    15.8 +
    15.9 +<HTML>
   15.10 +
   15.11 +<HEAD>
   15.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   15.13 +  <TITLE>HOL/Lambda</TITLE>
   15.14 +</HEAD>
   15.15 +
   15.16  <BODY>
   15.17  
   15.18  <H1>Lambda Calculus in de Bruijn's Notation</H1>
    16.1 --- a/src/HOL/Library/README.html	Mon Mar 07 18:40:36 2005 +0100
    16.2 +++ b/src/HOL/Library/README.html	Mon Mar 07 19:17:07 2005 +0100
    16.3 @@ -1,10 +1,13 @@
    16.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    16.5  
    16.6 +<!-- $Id$ -->
    16.7 +
    16.8  <html>
    16.9  
   16.10 -<!-- $Id$ -->
   16.11 -
   16.12 -<head><title>HOL-Library/README</title></head>
   16.13 +<head>
   16.14 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   16.15 +  <title>HOL-Library/README</title>
   16.16 +</head>
   16.17  
   16.18  <body>
   16.19  
    17.1 --- a/src/HOL/Modelcheck/README.html	Mon Mar 07 18:40:36 2005 +0100
    17.2 +++ b/src/HOL/Modelcheck/README.html	Mon Mar 07 19:17:07 2005 +0100
    17.3 @@ -1,10 +1,13 @@
    17.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    17.5  
    17.6 +<!-- $Id$ -->
    17.7 +
    17.8  <html>
    17.9  
   17.10 -<!-- $Id$ -->
   17.11 -
   17.12 -<head><title>HOL/Modelcheck</title></head>
   17.13 +<head>
   17.14 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   17.15 +  <title>HOL/Modelcheck</title>
   17.16 +</head>
   17.17  
   17.18  <body>
   17.19  
    18.1 --- a/src/HOL/Prolog/README.html	Mon Mar 07 18:40:36 2005 +0100
    18.2 +++ b/src/HOL/Prolog/README.html	Mon Mar 07 19:17:07 2005 +0100
    18.3 @@ -1,15 +1,20 @@
    18.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    18.5  
    18.6  <!-- $Id$ -->
    18.7 -<HTML><HEAD>
    18.8 -<TITLE>HOL/Prolog/README</TITLE>
    18.9 -</HEAD><BODY>
   18.10 +
   18.11 +<HTML>
   18.12  
   18.13 +<HEAD>
   18.14 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   18.15 +  <TITLE>HOL/Prolog/README</TITLE>
   18.16 +</HEAD>
   18.17 +
   18.18 +<BODY>
   18.19  <H2>Prolog -- A bare-bones implementation of Lambda-Prolog</H2>
   18.20  
   18.21 -This is a simple exploratory implementatin of 
   18.22 +This is a simple exploratory implementation of 
   18.23  <A HREF="http://www.cse.psu.edu/~dale/lProlog/">Lambda-Prolog</A> in HOL,
   18.24  including some minimal examples (in Test.thy) and a more typical example
   18.25  of a little functional language and its type system.
   18.26 -
   18.27 -</BODY></HTML>
   18.28 +</BODY>
   18.29 +</HTML>
    19.1 --- a/src/HOL/README.html	Mon Mar 07 18:40:36 2005 +0100
    19.2 +++ b/src/HOL/README.html	Mon Mar 07 19:17:07 2005 +0100
    19.3 @@ -1,10 +1,13 @@
    19.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    19.5  
    19.6 +<!-- $Id$ -->
    19.7 +
    19.8  <html>
    19.9  
   19.10 -<!-- $Id$ -->
   19.11 -
   19.12 -<head><title>HOL/README</title></head>
   19.13 +<head>
   19.14 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   19.15 +  <title>HOL/README</title>
   19.16 +</head>
   19.17  
   19.18  <body>
   19.19  
    20.1 --- a/src/HOL/Real/HahnBanach/README.html	Mon Mar 07 18:40:36 2005 +0100
    20.2 +++ b/src/HOL/Real/HahnBanach/README.html	Mon Mar 07 19:17:07 2005 +0100
    20.3 @@ -1,6 +1,15 @@
    20.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    20.5  
    20.6 -<HTML><HEAD><TITLE>HOL/Real/HahnBanach/README</TITLE></HEAD><BODY>
    20.7 +<!-- $Id$ -->
    20.8 +
    20.9 +<HTML>
   20.10 +
   20.11 +<HEAD>
   20.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   20.13 +  <TITLE>HOL/Real/HahnBanach/README</TITLE>
   20.14 +</HEAD>
   20.15 +
   20.16 +<BODY>
   20.17  
   20.18  <H3>The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)</H3>
   20.19  
   20.20 @@ -25,5 +34,5 @@
   20.21  <A NAME="bauerg@in.tum.de" HREF="mailto:bauerg@in.tum.de">bauerg@in.tum.de</A>
   20.22  </ADDRESS>
   20.23  
   20.24 -</BODY></HTML>
   20.25 -
   20.26 +</BODY>
   20.27 +</HTML>
    21.1 --- a/src/HOL/TLA/README.html	Mon Mar 07 18:40:36 2005 +0100
    21.2 +++ b/src/HOL/TLA/README.html	Mon Mar 07 19:17:07 2005 +0100
    21.3 @@ -1,6 +1,15 @@
    21.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    21.5  
    21.6 -<HTML><HEAD><TITLE>HOL/TLA</TITLE></HEAD><BODY>
    21.7 +<!-- $Id$ -->
    21.8 +
    21.9 +<HTML>
   21.10 +
   21.11 +<HEAD>
   21.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   21.13 +  <TITLE>HOL/TLA</TITLE>
   21.14 +</HEAD>
   21.15 +
   21.16 +<BODY>
   21.17  
   21.18  <H2>TLA: Lamport's Temporal Logic of Actions</H2>
   21.19  
   21.20 @@ -56,6 +65,6 @@
   21.21  <A HREF="merz@informatik.uni-muenchen.de">Stephan Merz</A>
   21.22  </ADDRESS>
   21.23  <!-- hhmts start -->
   21.24 -Last modified: Mon Jan 25 14:06:43 MET 1999
   21.25 +Last modified: Sat Mar  5 00:54:49 CET 2005
   21.26  <!-- hhmts end -->
   21.27  </BODY></HTML>
    22.1 --- a/src/HOL/UNITY/Comp/README.html	Mon Mar 07 18:40:36 2005 +0100
    22.2 +++ b/src/HOL/UNITY/Comp/README.html	Mon Mar 07 19:17:07 2005 +0100
    22.3 @@ -1,7 +1,15 @@
    22.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    22.5  
    22.6  <!-- $Id$ -->
    22.7 -<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
    22.8 +
    22.9 +<HTML>
   22.10 +
   22.11 +<HEAD>
   22.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   22.13 +  <TITLE>HOL/UNITY/README</TITLE>
   22.14 +</HEAD>
   22.15 +
   22.16 +<BODY>
   22.17  
   22.18  <H2>UNITY: Examples Involving Program Composition</H2>
   22.19  
   22.20 @@ -38,4 +46,5 @@
   22.21  <ADDRESS>
   22.22  <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
   22.23  </ADDRESS>
   22.24 -</BODY></HTML>
   22.25 +</BODY>
   22.26 +</HTML>
    23.1 --- a/src/HOL/UNITY/README.html	Mon Mar 07 18:40:36 2005 +0100
    23.2 +++ b/src/HOL/UNITY/README.html	Mon Mar 07 19:17:07 2005 +0100
    23.3 @@ -1,7 +1,15 @@
    23.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    23.5  
    23.6  <!-- $Id$ -->
    23.7 -<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
    23.8 +
    23.9 +<HTML>
   23.10 +
   23.11 +<HEAD>
   23.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   23.13 +  <TITLE>HOL/UNITY/README</TITLE>
   23.14 +</HEAD>
   23.15 +
   23.16 +<BODY>
   23.17  
   23.18  <H2>UNITY--Chandy and Misra's UNITY formalism</H2>
   23.19  
    24.1 --- a/src/HOL/UNITY/Simple/README.html	Mon Mar 07 18:40:36 2005 +0100
    24.2 +++ b/src/HOL/UNITY/Simple/README.html	Mon Mar 07 19:17:07 2005 +0100
    24.3 @@ -1,7 +1,15 @@
    24.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    24.5  
    24.6  <!-- $Id$ -->
    24.7 -<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
    24.8 +
    24.9 +<HTML>
   24.10 +
   24.11 +<HEAD>
   24.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   24.13 +  <TITLE>HOL/UNITY/README</TITLE>
   24.14 +</HEAD>
   24.15 +
   24.16 +<BODY>
   24.17  
   24.18  <H2>UNITY: Examples Involving Single Programs</H2>
   24.19  
   24.20 @@ -35,4 +43,5 @@
   24.21  <ADDRESS>
   24.22  <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
   24.23  </ADDRESS>
   24.24 -</BODY></HTML>
   24.25 +</BODY>
   24.26 +</HTML>
    25.1 --- a/src/HOL/W0/README.html	Mon Mar 07 18:40:36 2005 +0100
    25.2 +++ b/src/HOL/W0/README.html	Mon Mar 07 19:17:07 2005 +0100
    25.3 @@ -1,6 +1,14 @@
    25.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    25.5  
    25.6 -<HTML><HEAD><TITLE>HOL/W0/README</TITLE></HEAD>
    25.7 +<!-- $Id$ -->
    25.8 +
    25.9 +<HTML>
   25.10 +
   25.11 +<HEAD>
   25.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   25.13 +  <TITLE>HOL/W0/README</TITLE>
   25.14 +</HEAD>
   25.15 +
   25.16  <BODY>
   25.17  
   25.18  <H1>Type Inference for MiniML (without <tt>let</tt>)</H1>
    26.1 --- a/src/HOL/ex/README.html	Mon Mar 07 18:40:36 2005 +0100
    26.2 +++ b/src/HOL/ex/README.html	Mon Mar 07 19:17:07 2005 +0100
    26.3 @@ -1,7 +1,15 @@
    26.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    26.5  
    26.6  <!-- $Id$ -->
    26.7 -<HTML><HEAD><TITLE>HOL/ex/README</TITLE></HEAD><BODY>
    26.8 +
    26.9 +<HTML>
   26.10 +
   26.11 +<HEAD>
   26.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   26.13 +  <TITLE>HOL/ex/README</TITLE>
   26.14 +</HEAD>
   26.15 +
   26.16 +<BODY>
   26.17  
   26.18  <H2>ex--Miscellaneous Examples</H2>
   26.19  
   26.20 @@ -41,4 +49,5 @@
   26.21  <ADDRESS>
   26.22  <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
   26.23  </ADDRESS>
   26.24 -</BODY></HTML>
   26.25 +</BODY>
   26.26 +</HTML>
    27.1 --- a/src/HOLCF/FOCUS/README.html	Mon Mar 07 18:40:36 2005 +0100
    27.2 +++ b/src/HOLCF/FOCUS/README.html	Mon Mar 07 19:17:07 2005 +0100
    27.3 @@ -1,6 +1,13 @@
    27.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    27.5  
    27.6 -<HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
    27.7 +<HTML>
    27.8 +
    27.9 +<HEAD>
   27.10 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   27.11 +  <TITLE>HOLCF/README</TITLE>
   27.12 +</HEAD>
   27.13 +
   27.14 +<BODY>
   27.15  
   27.16  <H3>FOCUS: a theory of stream-processing functions Isabelle/<A HREF="..">HOLCF</A></H3>
   27.17  
    28.1 --- a/src/HOLCF/IMP/README.html	Mon Mar 07 18:40:36 2005 +0100
    28.2 +++ b/src/HOLCF/IMP/README.html	Mon Mar 07 19:17:07 2005 +0100
    28.3 @@ -1,10 +1,20 @@
    28.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    28.5  
    28.6 -<HTML><HEAD><TITLE>HOLCF/IMP/README</TITLE></HEAD><BODY>
    28.7 +<!-- $Id$ -->
    28.8 +
    28.9 +<HTML>
   28.10 +
   28.11 +<HEAD>
   28.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   28.13 +  <TITLE>HOLCF/IMP/README</TITLE>
   28.14 +</HEAD>
   28.15 +
   28.16 +<BODY>
   28.17  
   28.18  <H2>IMP -- A <KBD>WHILE</KBD>-language and its Semantics</H2>
   28.19  
   28.20  This is the HOLCF-based denotational semantics of a simple
   28.21  <tt>WHILE</tt>-language.  For a full description see <A
   28.22  HREF="../../HOL/IMP/index.html">HOL/IMP</A>.
   28.23 -</BODY></HTML>
   28.24 +</BODY>
   28.25 +</HTML>
    29.1 --- a/src/HOLCF/IOA/README.html	Mon Mar 07 18:40:36 2005 +0100
    29.2 +++ b/src/HOLCF/IOA/README.html	Mon Mar 07 19:17:07 2005 +0100
    29.3 @@ -1,6 +1,15 @@
    29.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    29.5  
    29.6 -<HTML><HEAD><TITLE>HOLCF/IOA/README</TITLE></HEAD><BODY>
    29.7 +<!-- $Id$ -->
    29.8 +
    29.9 +<HTML>
   29.10 +
   29.11 +<HEAD>
   29.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   29.13 +  <TITLE>HOLCF/IOA/README</TITLE>
   29.14 +</HEAD>
   29.15 +
   29.16 +<BODY>
   29.17  
   29.18  <H3>IOA: A formalization of I/O automata in HOLCF</H3>
   29.19  
    30.1 --- a/src/HOLCF/README.html	Mon Mar 07 18:40:36 2005 +0100
    30.2 +++ b/src/HOLCF/README.html	Mon Mar 07 19:17:07 2005 +0100
    30.3 @@ -1,8 +1,17 @@
    30.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    30.5  
    30.6 -<HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
    30.7 +<!-- $Id$ -->
    30.8 +
    30.9 +<html>
   30.10  
   30.11 -<H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
   30.12 +<head>
   30.13 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   30.14 +  <title>HOLCF/README</title>
   30.15 +</head>
   30.16 +
   30.17 +<body>
   30.18 +
   30.19 +<h3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</h3>
   30.20  
   30.21  HOLCF is the definitional extension of Church's Higher-Order Logic with
   30.22  Scott's Logic for Computable Functions that has been implemented in the
   30.23 @@ -10,25 +19,29 @@
   30.24  about functional programs. HOLCF supports standard domain theory (in particular
   30.25  fixpoint reasoning and recursive domain equations) but also coinductive
   30.26  arguments about lazy datatypes.
   30.27 -<P>
   30.28 +
   30.29 +<p>
   30.30 +
   30.31  The most recent description of HOLCF is found here:
   30.32 -<UL>
   30.33 -<li> <A HREF="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</A>
   30.34 -</UL>
   30.35  
   30.36 -A detailed description (in german) of the entire development can be found in:
   30.37 +<ul>
   30.38 +  <li><a href="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</a>
   30.39 +</ul>
   30.40  
   30.41 -<UL>
   30.42 -  <li> <A HREF="http://www4.informatik.tu-muenchen.de/publ/papers/Diss_Regensbu.pdf"> HOLCF: eine konservative Erweiterung von HOL um LCF</A>, <br>
   30.43 -        <A HREF="http://www4.informatik.tu-muenchen.de/~regensbu/">
   30.44 -        Franz Regenburger</A>. <br>
   30.45 -        Dissertation Technische Universit&auml;t M&uuml;nchen. <BR>
   30.46 -        Year: 1994.
   30.47 -</UL>
   30.48 +A detailed description (in German) of the entire development can be found in:
   30.49 +
   30.50 +<ul>
   30.51 +  <li><a href="http://www4.informatik.tu-muenchen.de/publ/papers/Diss_Regensbu.pdf">HOLCF: eine konservative Erweiterung von HOL um LCF</a>, <br>
   30.52 +      <a href="http://www4.informatik.tu-muenchen.de/~regensbu/">Franz Regenburger</a>.<br>
   30.53 +      Dissertation Technische Universit&auml;t M&uuml;nchen.<br>
   30.54 +      Year: 1994.
   30.55 +</ul>
   30.56  
   30.57  A short survey is available in:
   30.58 -<UL>
   30.59 -<li><A HREF="http://www4.informatik.tu-muenchen.de/publ/papers/Regensburger_HOLT1995.pdf">HOLCF: Higher Order Logic of Computable Functions</A> <br>
   30.60 -</UL>
   30.61 +<ul>
   30.62 +  <li><a href="http://www4.informatik.tu-muenchen.de/publ/papers/Regensburger_HOLT1995.pdf">HOLCF: Higher Order Logic of Computable Functions</a><br>
   30.63 +</ul>
   30.64  
   30.65 -</BODY></HTML>
   30.66 +</body>
   30.67 +
   30.68 +</html>
    31.1 --- a/src/LCF/README.html	Mon Mar 07 18:40:36 2005 +0100
    31.2 +++ b/src/LCF/README.html	Mon Mar 07 19:17:07 2005 +0100
    31.3 @@ -1,6 +1,15 @@
    31.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    31.5  
    31.6 -<HTML><HEAD><TITLE>LCF/README</TITLE></HEAD><BODY>
    31.7 +<!-- $Id$ -->
    31.8 +
    31.9 +<HTML>
   31.10 +
   31.11 +<HEAD>
   31.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   31.13 +  <TITLE>LCF/README</TITLE>
   31.14 +</HEAD>
   31.15 +
   31.16 +<BODY>
   31.17  
   31.18  <H2>LCF: Logic for Computable Functions</H2>
   31.19  
    32.1 --- a/src/Sequents/README.html	Mon Mar 07 18:40:36 2005 +0100
    32.2 +++ b/src/Sequents/README.html	Mon Mar 07 19:17:07 2005 +0100
    32.3 @@ -1,7 +1,15 @@
    32.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    32.5  
    32.6  <!-- $Id$ -->
    32.7 -<HTML><HEAD><TITLE>Sequents/README</TITLE></HEAD><BODY>
    32.8 +
    32.9 +<HTML>
   32.10 +
   32.11 +<HEAD>
   32.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   32.13 +  <TITLE>Sequents/README</TITLE>
   32.14 +</HEAD>
   32.15 +
   32.16 +<BODY>
   32.17  
   32.18  <H2>Sequents: Various Sequent Calculi</H2>
   32.19  
    33.1 --- a/src/ZF/AC/README.html	Mon Mar 07 18:40:36 2005 +0100
    33.2 +++ b/src/ZF/AC/README.html	Mon Mar 07 19:17:07 2005 +0100
    33.3 @@ -1,7 +1,15 @@
    33.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    33.5  
    33.6  <!-- $Id$ -->
    33.7 -<HTML><HEAD><TITLE>ZF/AC/README</TITLE></HEAD><BODY>
    33.8 +
    33.9 +<HTML>
   33.10 +
   33.11 +<HEAD>
   33.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   33.13 +  <TITLE>ZF/AC/README</TITLE>
   33.14 +</HEAD>
   33.15 +
   33.16 +<BODY>
   33.17  
   33.18  <H2>AC -- Equivalents of the Axiom of Choice</H2>
   33.19  
   33.20 @@ -9,7 +17,7 @@
   33.21  
   33.22  <P>
   33.23  <PRE>
   33.24 -@book{rubin&rubin,
   33.25 +@book{rubin&amp;rubin,
   33.26    author	= "Herman Rubin and Jean E. Rubin",
   33.27    title		= "Equivalents of the Axiom of Choice, {II}",
   33.28    publisher	= "North-Holland",
    34.1 --- a/src/ZF/Coind/README.html	Mon Mar 07 18:40:36 2005 +0100
    34.2 +++ b/src/ZF/Coind/README.html	Mon Mar 07 19:17:07 2005 +0100
    34.3 @@ -1,7 +1,15 @@
    34.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    34.5  
    34.6  <!-- $Id$ -->
    34.7 -<HTML><HEAD><TITLE>ZF/Coind/README</TITLE></HEAD><BODY>
    34.8 +
    34.9 +<HTML>
   34.10 +
   34.11 +<HEAD>
   34.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   34.13 +  <TITLE>ZF/Coind/README</TITLE>
   34.14 +</HEAD>
   34.15 +
   34.16 +<BODY>
   34.17  
   34.18  <H2>Coind -- A Coinduction Example</H2>
   34.19  
    35.1 --- a/src/ZF/Constructible/README.html	Mon Mar 07 18:40:36 2005 +0100
    35.2 +++ b/src/ZF/Constructible/README.html	Mon Mar 07 19:17:07 2005 +0100
    35.3 @@ -1,30 +1,41 @@
    35.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    35.5  
    35.6 -<HTML><HEAD><TITLE>ZF/Constructible/README</TITLE></HEAD><BODY>
    35.7 +<!-- $Id$ -->
    35.8 +
    35.9 +<html>
   35.10  
   35.11 -<H1>Constructible--Relative Consistency of the Axiom of Choice</H1>
   35.12 +<head>
   35.13 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   35.14 +  <title>ZF/Constructible/README</title>
   35.15 +</head>
   35.16  
   35.17 -<P>G&ouml;del's proof of the relative consistency of the axiom of choice is
   35.18 +<body>
   35.19 +<h1>Constructible--Relative Consistency of the Axiom of Choice</h1>
   35.20 +
   35.21 +G&ouml;del's proof of the relative consistency of the axiom of choice is
   35.22  mechanized using Isabelle/ZF.  The proof builds upon a previous mechanization
   35.23  of the
   35.24 -<A HREF="http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf">reflection
   35.25 -theorem</A>.  The heavy reliance on metatheory in the original proof makes the
   35.26 +<a href="http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf">reflection
   35.27 +theorem</a>.  The heavy reliance on metatheory in the original proof makes the
   35.28  formalization unusually long, and not entirely satisfactory: two parts of the
   35.29  proof do not fit together.  It seems impossible to solve these problems
   35.30  without formalizing the metatheory.  However, the present development follows
   35.31 -a standard textbook, Kunen's <STRONG>Set Theory</STRONG>, and could support the
   35.32 +a standard textbook, Kunen's <strong>Set Theory</strong>, and could support the
   35.33  formalization of further material from that book.  It also serves as an
   35.34  example of what to expect when deep mathematics is formalized.  
   35.35  
   35.36  A paper describing this development is
   35.37 -<A HREF="http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf">available</A>.
   35.38 +<a href="http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf">available</a>.
   35.39  
   35.40 -<HR>
   35.41 -<P>Last modified $Date$
   35.42 +<hr>
   35.43 +
   35.44 +<p>
   35.45  
   35.46 -<ADDRESS>
   35.47 -<A
   35.48 -HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
   35.49 -<A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
   35.50 -</ADDRESS>
   35.51 -</BODY></HTML>
   35.52 +Last modified $Date$
   35.53 +
   35.54 +<address>
   35.55 +<a href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>,
   35.56 +<a href="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</a>
   35.57 +</address>
   35.58 +</body>
   35.59 +</html>
    36.1 --- a/src/ZF/IMP/README.html	Mon Mar 07 18:40:36 2005 +0100
    36.2 +++ b/src/ZF/IMP/README.html	Mon Mar 07 19:17:07 2005 +0100
    36.3 @@ -1,7 +1,15 @@
    36.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    36.5  
    36.6  <!-- $Id$ -->
    36.7 -<HTML><HEAD><TITLE>ZF/IMP/README</TITLE></HEAD><BODY>
    36.8 +
    36.9 +<HTML>
   36.10 +
   36.11 +<HEAD>
   36.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   36.13 +  <TITLE>ZF/IMP/README</TITLE>
   36.14 +</HEAD>
   36.15 +
   36.16 +<BODY>
   36.17  
   36.18  <H2>IMP -- A <KBD>while</KBD>-language and two semantics</H2>
   36.19  
    37.1 --- a/src/ZF/README.html	Mon Mar 07 18:40:36 2005 +0100
    37.2 +++ b/src/ZF/README.html	Mon Mar 07 19:17:07 2005 +0100
    37.3 @@ -1,6 +1,15 @@
    37.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    37.5  
    37.6 -<HTML><HEAD><TITLE>ZF/README</TITLE></HEAD><BODY>
    37.7 +<!-- $Id$ -->
    37.8 +
    37.9 +<HTML>
   37.10 +
   37.11 +<HEAD>
   37.12 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   37.13 +  <TITLE>ZF/README</TITLE>
   37.14 +</HEAD>
   37.15 +
   37.16 +<BODY>
   37.17  
   37.18  <H2>ZF: Zermelo-Fraenkel Set Theory</H2>
   37.19  
    38.1 --- a/src/ZF/Resid/README.html	Mon Mar 07 18:40:36 2005 +0100
    38.2 +++ b/src/ZF/Resid/README.html	Mon Mar 07 19:17:07 2005 +0100
    38.3 @@ -1,29 +1,36 @@
    38.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    38.5  
    38.6  <!-- $Id$ -->
    38.7 -<HTML><HEAD><TITLE>ZF/Resid/README</TITLE></HEAD><BODY>
    38.8 +
    38.9 +<html>
   38.10  
   38.11 -<H2>Resid -- A theory of residuals</H2>
   38.12 +<head>
   38.13 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   38.14 +  <title>ZF/Resid/README</title>
   38.15 +</head>
   38.16 +
   38.17 +<body>
   38.18 +
   38.19 +<h2>Resid -- A theory of residuals</h2>
   38.20  
   38.21  Ole Rasmussen has ported to Isabelle/ZF the Coq proofs described in the
   38.22  article
   38.23  
   38.24 -<P>
   38.25 -<PRE>
   38.26 +<p>
   38.27 +
   38.28 +<pre>
   38.29  @Article{huet-residual,
   38.30 -  author	= "{G\'erard} Huet",
   38.31 -  title		= "Residual Theory in $\lambda$-Calculus: A Formal
   38.32 -		  Development", 
   38.33 -  journal	= JFP,
   38.34 -  year		= 1994,
   38.35 -  volume	= 4,
   38.36 -  number	= 3,
   38.37 -  pages		= "371--394"}
   38.38 -</PRE>
   38.39 +  author  = "{G\'erard} Huet",
   38.40 +  title   = "Residual Theory in $\lambda$-Calculus: A Formal Development",
   38.41 +  journal = JFP,
   38.42 +  year    = 1994,
   38.43 +  volume  = 4,
   38.44 +  number  = 3,
   38.45 +  pages   = "371--394"}
   38.46 +</pre>
   38.47  
   38.48 -See Rasmussen's report
   38.49 -<A HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz">The Church-Rosser Theorem in Isabelle: A Proof Porting
   38.50 -		  Experiment</A>.
   38.51 +See Rasmussen's report <a
   38.52 +href="http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz">The Church-Rosser Theorem in Isabelle: A Proof Porting Experiment</a>.
   38.53  
   38.54  </body>
   38.55  </html>
    39.1 --- a/src/ZF/ex/README.html	Mon Mar 07 18:40:36 2005 +0100
    39.2 +++ b/src/ZF/ex/README.html	Mon Mar 07 19:17:07 2005 +0100
    39.3 @@ -1,16 +1,23 @@
    39.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    39.5  
    39.6  <!-- $Id$ -->
    39.7 -<HTML><HEAD><TITLE>ZF/ex/README</TITLE></HEAD><BODY>
    39.8 +
    39.9 +<html>
   39.10  
   39.11 -<H2>ZF general examples</H2>
   39.12 +<head>
   39.13 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   39.14 +  <title>ZF/ex/README</title>
   39.15 +</head>
   39.16  
   39.17 -<P>Examples on this directory include a simple form of Ramsey's theorem.  A
   39.18 -<A
   39.19 -HREF="http://www.cl.cam.ac.uk/Research/Reports/TR271-lcp-set-theory.dvi.Z">report</A>
   39.20 -is available.
   39.21 +<body>
   39.22 +
   39.23 +<h2>ZF general examples</h2>
   39.24  
   39.25 -<P>Several (co)inductive and (co)datatype definitions are presented.  <A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz">One report</A> describes the theoretical foundations of datatypes while <A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz">another</A> describes the package that automates their declaration.
   39.26 +Examples on this directory include a simple form of Ramsey's theorem.  A <a href="http://www.cl.cam.ac.uk/Research/Reports/TR271-lcp-set-theory.dvi.Z">report</a> is available.
   39.27 +
   39.28 +<p>
   39.29 +
   39.30 +Several (co)inductive and (co)datatype definitions are presented.  <a href="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz">One report</a> describes the theoretical foundations of datatypes while <a href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz">another</a> describes the package that automates their declaration.
   39.31  
   39.32  </body>
   39.33  </html>