--- a/src/HOL/Lambda/README.html Tue Mar 05 15:55:15 1996 +0100
+++ b/src/HOL/Lambda/README.html Tue Mar 05 16:27:01 1996 +0100
@@ -1,4 +1,4 @@
-<HTML><HEAD><TITLE>HOL/Lambda/ReadMe</TITLE></HEAD>
+<HTML><HEAD><TITLE>HOL/Lambda</TITLE></HEAD>
<BODY>
<H1>Lambda Calculus in de Bruijn's Notation</H1>
@@ -8,9 +8,10 @@
<P>
-A report describing the whole theory is found here:<br>
-<A HREF=http://www4.informatik.tu-muenchen.de/~nipkow/pubs/church-rosser.html>
-More Church-Rosser Proofs (in Isabelle/HOL)</A>.
+The report
+<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/church-rosser.html">
+More Church-Rosser Proofs (in Isabelle/HOL)</A>
+describes the whole theory.
</BODY>
</HTML>
--- a/src/ZF/IMP/README.html Tue Mar 05 15:55:15 1996 +0100
+++ b/src/ZF/IMP/README.html Tue Mar 05 16:27:01 1996 +0100
@@ -1,6 +1,7 @@
-<HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY>
+<!-- $Id$ -->
+<HTML><HEAD><TITLE>HOL/IMP</TITLE></HEAD><BODY>
-<H2>IMP --- A <KBD>while</KBD>-language and two semantics</H2>
+<H2>IMP -- A <KBD>while</KBD>-language and two semantics</H2>
The formalization of the denotational and operational semantics of
a simple while-language together with an equivalence proof between the two
@@ -15,10 +16,14 @@
year = 1993}.
</PRE>
<P>
-Some documentation is found
-<A HREF=http://www4.informatik.tu-muenchen.de/~nipkow/pubs/loetz-sand.dvi.gz>
-here</A>
+There is a
+<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/loetz-sand.dvi.gz">
+report</A> by Lötzbeyer and Sandner.
<P>
A much extended version of this development is found in
-<A HREF=../../HOL/IMP/index.html>HOL/IMP</A>.
+<A HREF="../../HOL/IMP/index.html">HOL/IMP</A>.
</BODY></HTML>
+
+<HR>
+
+<P>Last modified 5 March 1996