NEWS
changeset 51775 408d937c9486
parent 51774 916271d52466
child 52052 892061142ba6
     1.1 --- a/NEWS	Thu Apr 25 10:35:56 2013 +0200
     1.2 +++ b/NEWS	Thu Apr 25 11:59:21 2013 +0200
     1.3 @@ -106,6 +106,9 @@
     1.4    conditionally_complete_lattice for real. Renamed lemmas about
     1.5    conditionally-complete lattice from Sup_... to cSup_... and from Inf_...
     1.6    to cInf_... to avoid hidding of similar complete lattice lemmas.
     1.7 +
     1.8 +  Introduce type class linear_continuum as combination of conditionally-complete
     1.9 +  lattices and inner dense linorders which have more than one element.
    1.10  INCOMPATIBILITY.
    1.11  
    1.12  * Introduce type classes "no_top" and "no_bot" for orderings without top
    1.13 @@ -116,8 +119,9 @@
    1.14  * Complex_Main: Unify and move various concepts from
    1.15    HOL-Multivariate_Analysis to HOL-Complex_Main.
    1.16  
    1.17 - - Introduce type class (lin)order_topology. Allows to generalize theorems
    1.18 -   about limits and order. Instances are reals and extended reals.
    1.19 + - Introduce type class (lin)order_topology and linear_continuum_topology.
    1.20 +   Allows to generalize theorems about limits and order.
    1.21 +   Instances are reals and extended reals.
    1.22  
    1.23   - continuous and continuos_on from Multivariate_Analysis:
    1.24     "continuous" is the continuity of a function at a filter.
    1.25 @@ -132,9 +136,8 @@
    1.26     function is continuous, when the function is continuous on a compact set.
    1.27  
    1.28   - connected from Multivariate_Analysis. Use it to prove the
    1.29 -   intermediate value theorem. Show connectedness of intervals on order
    1.30 -   topologies which are a inner dense, conditionally-complete linorder
    1.31 -   (named connected_linorder_topology).
    1.32 +   intermediate value theorem. Show connectedness of intervals on
    1.33 +   linear_continuum_topology).
    1.34  
    1.35   - first_countable_topology from Multivariate_Analysis. Is used to
    1.36     show equivalence of properties on the neighbourhood filter of x and on