NEWS
changeset 62101 26c0a70f78a3
parent 62098 b1b2834bb493
child 62111 e2b768b0035d
     1.1 --- a/NEWS	Fri Jan 08 16:37:56 2016 +0100
     1.2 +++ b/NEWS	Fri Jan 08 17:40:59 2016 +0100
     1.3 @@ -606,6 +606,14 @@
     1.4  terms for sup and inf. For example, "sup x (sup y (- x))" simplifies to
     1.5  "top". INCOMPATIBILITY.
     1.6  
     1.7 +* Class uniform_space introduces uniform spaces btw topological spaces
     1.8 +and metric spaces. Minor INCOMPATIBILITY: open_<type>_def needs to be
     1.9 +introduced in the form of an uniformity. Some constants are more
    1.10 +general now, it may be necessary to add type class constraints.
    1.11 +
    1.12 +  open_real_def \<leadsto> open_dist
    1.13 +  open_complex_def \<leadsto> open_dist
    1.14 +
    1.15  * Library/Monad_Syntax: notation uses symbols \<bind> and \<then>. INCOMPATIBILITY.
    1.16  
    1.17  * Library/Multiset: