--- a/src/HOL/IMP/README.html Sat Apr 27 12:09:21 1996 +0200
+++ b/src/HOL/IMP/README.html Sat Apr 27 18:47:31 1996 +0200
@@ -1,21 +1,18 @@
<HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY>
-<H2>IMP --- A <KBD>while</KBD>-language and its 3 Semantics</H2>
+<H2>IMP --- A <KBD>WHILE</KBD>-language and its Semantics</H2>
-The formalization of the denotational, operational and axiomatic semantics of
-a simple while-language, including
-<UL>
-<LI> an equivalence proof between denotational and operational semantics and
-<LI> a soundness proof of the Hoare rules w.r.t. the denotational semantics.
-</UL>
-The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of
-<P>
-<KBD>
+The denotational, operational, and axiomatic semantics, a verification
+condition generator, and all the necessary soundness, completeness and
+equivalence proofs. Essentially a formalization of the first 100 pages
+of
+<PRE>
@book{Winskel, author = {Glynn Winskel},
title = {The Formal Semantics of Programming Languages},
publisher = {MIT Press}, year = 1993}
-</KBD>
+</PRE>
<P>
-In addition, a verification-condition-generator is proved sound and complete
-w.r.t. the Hoare rules.
+An eminently readable description of this theory is found
+<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/imp.html">
+here</A>.
</BODY></HTML>