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

author | nipkow |

Tue, 23 May 2000 09:08:18 +0200 | |

changeset 8925 | f4599af94b83 |

parent 8924 | c434283b4cfa |

child 8926 | 0c7f90147f5d |

SetInterval

--- a/NEWS Tue May 23 07:32:24 2000 +0200 +++ b/NEWS Tue May 23 09:08:18 2000 +0200 @@ -161,6 +161,9 @@ individually as well, resulting in a separate list of theorems for each equation; +* HOL: new (overloaded) notation for the set of elements below/above some +element: {..u}, {..u(}, {l..}, {)l..}. See theory SetInterval. + * HOL: theorems impI, allI, ballI bound as "strip"; * theory Sexp now in HOL/Induct examples (used to be part of main HOL,