# HG changeset patch
# User nipkow
# Date 964782299 -7200
# Node ID 966974a7a5b32c33b7fb8a553806654c7b010a30
# Parent  880794f48ce6b86a5723a90127afff4af3a5ce3f
* HOL/While

diff -r 880794f48ce6 -r 966974a7a5b3 NEWS
--- a/NEWS	Thu Jul 27 18:27:25 2000 +0200
+++ b/NEWS	Fri Jul 28 13:04:59 2000 +0200
@@ -237,6 +237,11 @@
 individually as well, resulting in a separate list of theorems for
 each equation;
 
+* HOL/While is a new theory that provides a while-combinator. It permits the
+definition of tail-recursive functions without the provision of a termination
+measure. The latter is necessary once the invariant proof rule for while is
+applied.
+
 * HOL: new (overloaded) notation for the set of elements below/above some
 element: {..u}, {..u(}, {l..}, {)l..}. See theory SetInterval.