NEWS

--- a/NEWS	Fri Oct 06 16:14:03 2000 +0200
+++ b/NEWS	Fri Oct 06 16:18:30 2000 +0200
@@ -257,6 +257,9 @@
 * HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog, by David
 von Oheimb;
 
+* HOL/IMPP: extension of IMP with local variables and mutually
+recursive procedures, by David von Oheimb;
+
 * HOL/Lambda: converted into new-style theory and document;
 
 * HOL/ex/Multiquote: example of multiple nested quotations and