# HG changeset patch
# User nipkow
# Date 825444516 -3600
# Node ID 4093c3cb7b30188537250a5f78500e86584e3c10
# Parent 4ed3004ff75e5196d9be3895bc3fa2444e80e6af
Added documentation
diff -r 4ed3004ff75e -r 4093c3cb7b30 src/ZF/IMP/README.html
--- /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 @@
+HOL/IMP/ReadMe
+
+IMP --- A while-language and two semantics
+
+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
+
+
+@book{Winskel,
+ author = {Glynn Winskel},
+ title = {The Formal Semantics of Programming Languages},
+ publisher = {MIT Press},
+ year = 1993}.
+
+
+Some documentation is found
+
+here
+
+A much extended version of this development is found in
+HOL/IMP.
+