--- a/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,9 +1,9 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+<!-- $Id$ -->
+
<html>
-<!-- $Id$ -->
-
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<title>The Isabelle System Distribution</title>
--- a/src/CTT/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/CTT/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>CTT/README</TITLE></HEAD><BODY>
+<!-- $Id$ -->
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>CTT/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>CTT: Constructive Type Theory</H2>
--- a/src/Cube/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/Cube/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>Cube/README</TITLE></HEAD><BODY>
+<!-- $Id$ -->
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>Cube/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>Cube: Barendregt's Lambda-Cube</H2>
--- a/src/FOL/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/FOL/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<html><head><title>FOL/README</title></head><body>
+<!-- $Id$ -->
+
+<html>
+
+<head>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <title>FOL/README</title>
+</head>
+
+<body>
<h2>FOL: First-Order Logic with Natural Deduction</h2>
@@ -19,4 +28,5 @@
<li>Antony Galton, Logic for Information Technology (Wiley, 1990)
<li>Michael Dummett, Elements of Intuitionism (Oxford, 1977)
</ul>
-</body></html>
+</body>
+</html>
--- a/src/HOL/Algebra/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Algebra/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
+ <TITLE>HOL/Algebra/README.html</TITLE>
+</HEAD>
+
+<BODY>
<H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1>
@@ -110,4 +118,5 @@
<ADDRESS>
<P><A HREF="http://www4.in.tum.de/~ballarin">Clemens Ballarin</A>.
</ADDRESS>
-</BODY></HTML>
+</BODY>
+</HTML>
--- a/src/HOL/Auth/Guard/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Auth/Guard/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/Auth/Guard/README.html</TITLE></HEAD><BODY>
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
+ <TITLE>HOL/Auth/Guard/README.html</TITLE>
+</HEAD>
+
+<BODY>
<H1>Protocol-Independent Secrecy Results</H1>
@@ -58,4 +66,5 @@
<A HREF="http://www.lri.fr/~blanqui/">Frederic Blanqui</A>,
<A HREF="mailto:blanqui@lri.fr">blanqui@lri.fr</A>
</ADDRESS>
-</BODY></HTML>
+</BODY>
+</HTML>
--- a/src/HOL/Auth/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Auth/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
+<!-- $Id$ -->
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
+ <TITLE>HOL/Auth/README</TITLE>
+</HEAD>
+
+<BODY>
<H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
@@ -45,4 +54,5 @@
HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
<A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>
-</BODY></HTML>
+</BODY>
+</HTML>
--- a/src/HOL/AxClasses/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/AxClasses/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,10 +1,12 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
+
<html>
<head>
-<title>HOL/AxClasses</title>
+ <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
+ <title>HOL/AxClasses</title>
</head>
<body>
@@ -14,6 +16,5 @@
href="http://isabelle.in.tum.de/doc/axclass.pdf">Using Axiomatic Type
Classes in Isabelle</a>. See also FOL/ex/NatClass for the natural
number example.
-
</body>
</html>
--- a/src/HOL/Complex/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Complex/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,8 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>HOL/Complex/README</TITLE>
- <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
- </HEAD><BODY>
+<!-- $Id$ -->
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
+ <TITLE>HOL/Complex/README</TITLE>
+</HEAD>
+
+<BODY>
<H1>Complex: The Complex Numbers</H1>
<P>This directory defines the type <KBD>complex</KBD> of the complex numbers,
@@ -56,5 +63,5 @@
</ul>
<HR>
<P>Last modified $Date$
-
+</BODY>
</HTML>
--- a/src/HOL/Hoare/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Hoare/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>HOL/Hoare/ReadMe</TITLE></HEAD><BODY>
+<!-- $Id$ -->
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOL/Hoare/ReadMe</TITLE>
+</HEAD>
+
+<BODY>
<H2>Hoare Logic for a Simple WHILE Language</H2>
@@ -83,4 +92,5 @@
<P>
and the embeding is deep, i.e. there is a concrete datatype of programs. The
latter is not really necessary.
-</BODY></HTML>
+</BODY>
+</HTML>
--- a/src/HOL/IMPP/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/IMPP/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,9 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD>
-<TITLE>HOL/IMPP/README</TITLE>
-</HEAD><BODY>
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOL/IMPP/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>IMPP--An imperative language with procedures</H2>
--- a/src/HOL/IOA/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/IOA/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,18 +1,27 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>HOLCF/IOA/README</TITLE></HEAD><BODY>
+<!-- $Id -->
+
+<html>
+
+<head>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <title>HOLCF/IOA/README</title>
+</head>
-<H3>IOA: A basic formalization of I/O automata in HOL</H3>
+<body>
+
+<h3>IOA: A basic formalization of I/O automata in HOL</h3>
-Author: Konrad Slind, Tobias Nipkow and Olaf Müller<BR>
-Copyright 1995,1996 Technische Universität München<P>
+Author: Konrad Slind, Tobias Nipkow and Olaf Müller<br>
+Copyright 1995,1996 Technische Universität München
+
+<p>
This directory contains a formalization of the meta theory of I/O automata in HOL.
-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
-have been here.
-
+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 have been here.
-</BODY></HTML>
-
-
-
+</body>
+</html>
--- a/src/HOL/Induct/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Induct/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/Induct/README</TITLE></HEAD><BODY>
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOL/Induct/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>Induct--Examples of (Co)Inductive Definitions</H2>
--- a/src/HOL/Isar_examples/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Isar_examples/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,10 +1,12 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
+
<html>
<head>
-<title>HOL/Isar_examples</title>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <title>HOL/Isar_examples</title>
</head>
<body>
@@ -15,6 +17,5 @@
also the included document, or the <a
href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar page</a> for more
information.
-
</body>
</html>
--- a/src/HOL/Lambda/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Lambda/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,14 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/Lambda</TITLE></HEAD>
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOL/Lambda</TITLE>
+</HEAD>
+
<BODY>
<H1>Lambda Calculus in de Bruijn's Notation</H1>
--- a/src/HOL/Library/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Library/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,10 +1,13 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+<!-- $Id$ -->
+
<html>
-<!-- $Id$ -->
-
-<head><title>HOL-Library/README</title></head>
+<head>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <title>HOL-Library/README</title>
+</head>
<body>
--- a/src/HOL/Modelcheck/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Modelcheck/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,10 +1,13 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+<!-- $Id$ -->
+
<html>
-<!-- $Id$ -->
-
-<head><title>HOL/Modelcheck</title></head>
+<head>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <title>HOL/Modelcheck</title>
+</head>
<body>
--- a/src/HOL/Prolog/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Prolog/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,15 +1,20 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD>
-<TITLE>HOL/Prolog/README</TITLE>
-</HEAD><BODY>
+
+<HTML>
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOL/Prolog/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>Prolog -- A bare-bones implementation of Lambda-Prolog</H2>
-This is a simple exploratory implementatin of
+This is a simple exploratory implementation of
<A HREF="http://www.cse.psu.edu/~dale/lProlog/">Lambda-Prolog</A> in HOL,
including some minimal examples (in Test.thy) and a more typical example
of a little functional language and its type system.
-
-</BODY></HTML>
+</BODY>
+</HTML>
--- a/src/HOL/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,10 +1,13 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+<!-- $Id$ -->
+
<html>
-<!-- $Id$ -->
-
-<head><title>HOL/README</title></head>
+<head>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <title>HOL/README</title>
+</head>
<body>
--- a/src/HOL/Real/HahnBanach/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Real/HahnBanach/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>HOL/Real/HahnBanach/README</TITLE></HEAD><BODY>
+<!-- $Id$ -->
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOL/Real/HahnBanach/README</TITLE>
+</HEAD>
+
+<BODY>
<H3>The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)</H3>
@@ -25,5 +34,5 @@
<A NAME="bauerg@in.tum.de" HREF="mailto:bauerg@in.tum.de">bauerg@in.tum.de</A>
</ADDRESS>
-</BODY></HTML>
-
+</BODY>
+</HTML>
--- a/src/HOL/TLA/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/TLA/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>HOL/TLA</TITLE></HEAD><BODY>
+<!-- $Id$ -->
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOL/TLA</TITLE>
+</HEAD>
+
+<BODY>
<H2>TLA: Lamport's Temporal Logic of Actions</H2>
@@ -56,6 +65,6 @@
<A HREF="merz@informatik.uni-muenchen.de">Stephan Merz</A>
</ADDRESS>
<!-- hhmts start -->
-Last modified: Mon Jan 25 14:06:43 MET 1999
+Last modified: Sat Mar 5 00:54:49 CET 2005
<!-- hhmts end -->
</BODY></HTML>
--- a/src/HOL/UNITY/Comp/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/UNITY/Comp/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOL/UNITY/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>UNITY: Examples Involving Program Composition</H2>
@@ -38,4 +46,5 @@
<ADDRESS>
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>
-</BODY></HTML>
+</BODY>
+</HTML>
--- a/src/HOL/UNITY/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/UNITY/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOL/UNITY/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>UNITY--Chandy and Misra's UNITY formalism</H2>
--- a/src/HOL/UNITY/Simple/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/UNITY/Simple/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOL/UNITY/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>UNITY: Examples Involving Single Programs</H2>
@@ -35,4 +43,5 @@
<ADDRESS>
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>
-</BODY></HTML>
+</BODY>
+</HTML>
--- a/src/HOL/W0/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/W0/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,14 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>HOL/W0/README</TITLE></HEAD>
+<!-- $Id$ -->
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOL/W0/README</TITLE>
+</HEAD>
+
<BODY>
<H1>Type Inference for MiniML (without <tt>let</tt>)</H1>
--- a/src/HOL/ex/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/ex/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/ex/README</TITLE></HEAD><BODY>
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOL/ex/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>ex--Miscellaneous Examples</H2>
@@ -41,4 +49,5 @@
<ADDRESS>
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>
-</BODY></HTML>
+</BODY>
+</HTML>
--- a/src/HOLCF/FOCUS/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOLCF/FOCUS/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,13 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOLCF/README</TITLE>
+</HEAD>
+
+<BODY>
<H3>FOCUS: a theory of stream-processing functions Isabelle/<A HREF="..">HOLCF</A></H3>
--- a/src/HOLCF/IMP/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOLCF/IMP/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,10 +1,20 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>HOLCF/IMP/README</TITLE></HEAD><BODY>
+<!-- $Id$ -->
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOLCF/IMP/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>IMP -- A <KBD>WHILE</KBD>-language and its Semantics</H2>
This is the HOLCF-based denotational semantics of a simple
<tt>WHILE</tt>-language. For a full description see <A
HREF="../../HOL/IMP/index.html">HOL/IMP</A>.
-</BODY></HTML>
+</BODY>
+</HTML>
--- a/src/HOLCF/IOA/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOLCF/IOA/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>HOLCF/IOA/README</TITLE></HEAD><BODY>
+<!-- $Id$ -->
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>HOLCF/IOA/README</TITLE>
+</HEAD>
+
+<BODY>
<H3>IOA: A formalization of I/O automata in HOLCF</H3>
--- a/src/HOLCF/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOLCF/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,8 +1,17 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
+<!-- $Id$ -->
+
+<html>
-<H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
+<head>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <title>HOLCF/README</title>
+</head>
+
+<body>
+
+<h3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</h3>
HOLCF is the definitional extension of Church's Higher-Order Logic with
Scott's Logic for Computable Functions that has been implemented in the
@@ -10,25 +19,29 @@
about functional programs. HOLCF supports standard domain theory (in particular
fixpoint reasoning and recursive domain equations) but also coinductive
arguments about lazy datatypes.
-<P>
+
+<p>
+
The most recent description of HOLCF is found here:
-<UL>
-<li> <A HREF="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</A>
-</UL>
-A detailed description (in german) of the entire development can be found in:
+<ul>
+ <li><a href="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</a>
+</ul>
-<UL>
- <li> <A HREF="http://www4.informatik.tu-muenchen.de/publ/papers/Diss_Regensbu.pdf"> HOLCF: eine konservative Erweiterung von HOL um LCF</A>, <br>
- <A HREF="http://www4.informatik.tu-muenchen.de/~regensbu/">
- Franz Regenburger</A>. <br>
- Dissertation Technische Universität München. <BR>
- Year: 1994.
-</UL>
+A detailed description (in German) of the entire development can be found in:
+
+<ul>
+ <li><a href="http://www4.informatik.tu-muenchen.de/publ/papers/Diss_Regensbu.pdf">HOLCF: eine konservative Erweiterung von HOL um LCF</a>, <br>
+ <a href="http://www4.informatik.tu-muenchen.de/~regensbu/">Franz Regenburger</a>.<br>
+ Dissertation Technische Universität München.<br>
+ Year: 1994.
+</ul>
A short survey is available in:
-<UL>
-<li><A HREF="http://www4.informatik.tu-muenchen.de/publ/papers/Regensburger_HOLT1995.pdf">HOLCF: Higher Order Logic of Computable Functions</A> <br>
-</UL>
+<ul>
+ <li><a href="http://www4.informatik.tu-muenchen.de/publ/papers/Regensburger_HOLT1995.pdf">HOLCF: Higher Order Logic of Computable Functions</a><br>
+</ul>
-</BODY></HTML>
+</body>
+
+</html>
--- a/src/LCF/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/LCF/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>LCF/README</TITLE></HEAD><BODY>
+<!-- $Id$ -->
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>LCF/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>LCF: Logic for Computable Functions</H2>
--- a/src/Sequents/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/Sequents/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>Sequents/README</TITLE></HEAD><BODY>
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>Sequents/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>Sequents: Various Sequent Calculi</H2>
--- a/src/ZF/AC/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/AC/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>ZF/AC/README</TITLE></HEAD><BODY>
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>ZF/AC/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>AC -- Equivalents of the Axiom of Choice</H2>
@@ -9,7 +17,7 @@
<P>
<PRE>
-@book{rubin&rubin,
+@book{rubin&rubin,
author = "Herman Rubin and Jean E. Rubin",
title = "Equivalents of the Axiom of Choice, {II}",
publisher = "North-Holland",
--- a/src/ZF/Coind/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/Coind/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>ZF/Coind/README</TITLE></HEAD><BODY>
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>ZF/Coind/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>Coind -- A Coinduction Example</H2>
--- a/src/ZF/Constructible/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/Constructible/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,30 +1,41 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>ZF/Constructible/README</TITLE></HEAD><BODY>
+<!-- $Id$ -->
+
+<html>
-<H1>Constructible--Relative Consistency of the Axiom of Choice</H1>
+<head>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <title>ZF/Constructible/README</title>
+</head>
-<P>Gödel's proof of the relative consistency of the axiom of choice is
+<body>
+<h1>Constructible--Relative Consistency of the Axiom of Choice</h1>
+
+Gödel's proof of the relative consistency of the axiom of choice is
mechanized using Isabelle/ZF. The proof builds upon a previous mechanization
of the
-<A HREF="http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf">reflection
-theorem</A>. The heavy reliance on metatheory in the original proof makes the
+<a href="http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf">reflection
+theorem</a>. The heavy reliance on metatheory in the original proof makes the
formalization unusually long, and not entirely satisfactory: two parts of the
proof do not fit together. It seems impossible to solve these problems
without formalizing the metatheory. However, the present development follows
-a standard textbook, Kunen's <STRONG>Set Theory</STRONG>, and could support the
+a standard textbook, Kunen's <strong>Set Theory</strong>, and could support the
formalization of further material from that book. It also serves as an
example of what to expect when deep mathematics is formalized.
A paper describing this development is
-<A HREF="http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf">available</A>.
+<a href="http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf">available</a>.
-<HR>
-<P>Last modified $Date$
+<hr>
+
+<p>
-<ADDRESS>
-<A
-HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
-<A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
-</ADDRESS>
-</BODY></HTML>
+Last modified $Date$
+
+<address>
+<a href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>,
+<a href="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</a>
+</address>
+</body>
+</html>
--- a/src/ZF/IMP/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/IMP/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>ZF/IMP/README</TITLE></HEAD><BODY>
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>ZF/IMP/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>IMP -- A <KBD>while</KBD>-language and two semantics</H2>
--- a/src/ZF/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<HTML><HEAD><TITLE>ZF/README</TITLE></HEAD><BODY>
+<!-- $Id$ -->
+
+<HTML>
+
+<HEAD>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <TITLE>ZF/README</TITLE>
+</HEAD>
+
+<BODY>
<H2>ZF: Zermelo-Fraenkel Set Theory</H2>
--- a/src/ZF/Resid/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/Resid/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,29 +1,36 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>ZF/Resid/README</TITLE></HEAD><BODY>
+
+<html>
-<H2>Resid -- A theory of residuals</H2>
+<head>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <title>ZF/Resid/README</title>
+</head>
+
+<body>
+
+<h2>Resid -- A theory of residuals</h2>
Ole Rasmussen has ported to Isabelle/ZF the Coq proofs described in the
article
-<P>
-<PRE>
+<p>
+
+<pre>
@Article{huet-residual,
- author = "{G\'erard} Huet",
- title = "Residual Theory in $\lambda$-Calculus: A Formal
- Development",
- journal = JFP,
- year = 1994,
- volume = 4,
- number = 3,
- pages = "371--394"}
-</PRE>
+ author = "{G\'erard} Huet",
+ title = "Residual Theory in $\lambda$-Calculus: A Formal Development",
+ journal = JFP,
+ year = 1994,
+ volume = 4,
+ number = 3,
+ pages = "371--394"}
+</pre>
-See Rasmussen's report
-<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
- Experiment</A>.
+See Rasmussen's report <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 Experiment</a>.
</body>
</html>
--- a/src/ZF/ex/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/ex/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,16 +1,23 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- $Id$ -->
-<HTML><HEAD><TITLE>ZF/ex/README</TITLE></HEAD><BODY>
+
+<html>
-<H2>ZF general examples</H2>
+<head>
+ <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+ <title>ZF/ex/README</title>
+</head>
-<P>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.
+<body>
+
+<h2>ZF general examples</h2>
-<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.
+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.
+
+<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.
</body>
</html>