diff -r db112d36a426 -r e59e93ad85eb src/HOL/IMPP/README.html
--- /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 @@
+
+
+HOL/IMPP/README
+
+
+IMPP--An imperative language with procedures
+
+This is an extension of IMP with local variables
+and mutually recursive procedures. For documentation see
+
+Hoare Logic for Mutual Recursion and Local Variables.
+
+