NEWS
changeset 9457 966974a7a5b3
parent 9437 93e91040c286
child 9489 aa757b35b129
     1.1 --- a/NEWS	Thu Jul 27 18:27:25 2000 +0200
     1.2 +++ b/NEWS	Fri Jul 28 13:04:59 2000 +0200
     1.3 @@ -237,6 +237,11 @@
     1.4  individually as well, resulting in a separate list of theorems for
     1.5  each equation;
     1.6  
     1.7 +* HOL/While is a new theory that provides a while-combinator. It permits the
     1.8 +definition of tail-recursive functions without the provision of a termination
     1.9 +measure. The latter is necessary once the invariant proof rule for while is
    1.10 +applied.
    1.11 +
    1.12  * HOL: new (overloaded) notation for the set of elements below/above some
    1.13  element: {..u}, {..u(}, {l..}, {)l..}. See theory SetInterval.
    1.14