src/HOL/IMP/README.html
changeset 3124 1c0dfa7ebb72
parent 2796 c23e367e57be
     1.1 --- a/src/HOL/IMP/README.html	Wed May 07 13:50:18 1997 +0200
     1.2 +++ b/src/HOL/IMP/README.html	Wed May 07 13:50:52 1997 +0200
     1.3 @@ -1,6 +1,7 @@
     1.4 -<HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY>
     1.5 +<!-- $Id$ -->
     1.6 +<HTML><HEAD><TITLE>HOL/IMP/README</TITLE></HEAD><BODY>
     1.7  
     1.8 -<H2>IMP --- A <KBD>WHILE</KBD>-language and its Semantics</H2>
     1.9 +<H2>IMP--A <KBD>WHILE</KBD>-language and its Semantics</H2>
    1.10  
    1.11  The denotational, operational, and axiomatic semantics, a verification
    1.12  condition generator, and all the necessary soundness, completeness and
    1.13 @@ -18,4 +19,8 @@
    1.14  <P>
    1.15  A denotational semantics for IMP based on HOLCF is found
    1.16  <A HREF="../../HOLCF/IMP/index.html">here</A>.
    1.17 +
    1.18 +<HR>
    1.19 +<P>Last modified 7 May 1997
    1.20 +
    1.21  </BODY></HTML>