--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/README.html Tue Feb 27 19:08:36 1996 +0100
@@ -0,0 +1,24 @@
+<HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY>
+
+<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
+semantics. The whole development essentially formalizes/transcribes chapters
+2 and 5 of
+<P>
+<PRE>
+@book{Winskel,
+ author = {Glynn Winskel},
+ title = {The Formal Semantics of Programming Languages},
+ publisher = {MIT Press},
+ year = 1993}.
+</PRE>
+<P>
+Some documentation is found
+<A HREF=http://www4.informatik.tu-muenchen.de/~nipkow/pubs/loetz-sand.dvi.gz>
+here</A>
+<P>
+A much extended version of this development is found in
+<A HREF=../../HOL/IMP/index.html>HOL/IMP</A>.
+</BODY></HTML>