--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/README.html	Fri Nov 17 13:15:19 1995 +0100
@@ -0,0 +1,20 @@
+<HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY>
+
+<H2>IMP --- A <KBD>while</KBD>-Language and its 3 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> the derivation of the Hoare rules from the denotational semantics.
+</UL>
+The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of
+<P>
+<KBD>
+@book{Winskel,author={Glynn Winskel},
+title={The Formal Semantics of Programming Languages},
+publisher={MIT Press},year=1993}
+</KBD>
+<P>
+Here is the documentation.
+</BODY></HTML>