NEWS

   Allows to generalize some lemmas about reals and extended reals.
   Removed SupInf and replaced it by the instantiation of
   conditionally_complete_lattice for real. Renamed lemmas about
   conditionally-complete lattice from Sup_... to cSup_... and from Inf_...
   to cInf_... to avoid hidding of similar complete lattice lemmas.
+
+  Introduce type class linear_continuum as combination of conditionally-complete
+  lattices and inner dense linorders which have more than one element.
 INCOMPATIBILITY.
 
 * Introduce type classes "no_top" and "no_bot" for orderings without top
   and bottom elements.
 
 * Split dense_linorder into inner_dense_order and no_top, no_bot.
 
 * Complex_Main: Unify and move various concepts from
   HOL-Multivariate_Analysis to HOL-Complex_Main.
 
- - Introduce type class (lin)order_topology. Allows to generalize theorems
-   about limits and order. Instances are reals and extended reals.
+ - Introduce type class (lin)order_topology and linear_continuum_topology.
+   Allows to generalize theorems about limits and order.
+   Instances are reals and extended reals.
 
  - continuous and continuos_on from Multivariate_Analysis:
    "continuous" is the continuity of a function at a filter.
    "isCont" is now an abbrevitation: "isCont x f == continuous (at _) f".
 

    to prove compactness of closed intervals on reals. Continuous functions
    attain infimum and supremum on compact sets. The inverse of a continuous
    function is continuous, when the function is continuous on a compact set.
 
  - connected from Multivariate_Analysis. Use it to prove the
-   intermediate value theorem. Show connectedness of intervals on order
-   topologies which are a inner dense, conditionally-complete linorder
-   (named connected_linorder_topology).
+   intermediate value theorem. Show connectedness of intervals on
+   linear_continuum_topology).
 
  - first_countable_topology from Multivariate_Analysis. Is used to
    show equivalence of properties on the neighbourhood filter of x and on
    all sequences converging to x.