summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 28 Jul 2000 13:04:59 +0200 | |

changeset 9457 | 966974a7a5b3 |

parent 9456 | 880794f48ce6 |

child 9458 | c613cd06d5cf |

* HOL/While

--- 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.