summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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