diff -r 0f9b9eda2a2c -r e84bff5c519b src/HOL/IMP/README.html
--- 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 @@
HOL/IMP/ReadMe
-IMP --- A while-language and its 3 Semantics
+IMP --- A WHILE-language and its Semantics
-The formalization of the denotational, operational and axiomatic semantics of
-a simple while-language, including
-
-- an equivalence proof between denotational and operational semantics and
-
- a soundness proof of the Hoare rules w.r.t. the denotational semantics.
-
-The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of
-
-
+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
+
@book{Winskel, author = {Glynn Winskel},
title = {The Formal Semantics of Programming Languages},
publisher = {MIT Press}, year = 1993}
-
+
-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
+
+here.