summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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