--- 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