--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMPP/README.html	Mon Jan 31 18:30:35 2000 +0100
@@ -0,0 +1,13 @@
+<!-- $Id$ -->
+<HTML><HEAD>
+<TITLE>HOL/IMPP/README</TITLE>
+</HEAD><BODY>
+
+<H2>IMPP--An imperative language with procedures</H2>
+
+This is an extension of <A HREF="../IMP/">IMP</A> with local variables
+and mutually recursive procedures. For documentation see
+<A HREF="http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html">
+Hoare Logic for Mutual Recursion and Local Variables</A>.
+
+</BODY></HTML>