changeset 51732 4392eb046a97
parent 51717 9e7d1c139569
child 51747 e4b5bebe5235
--- a/NEWS	Sun Apr 21 20:08:13 2013 +0200
+++ b/NEWS	Mon Apr 22 16:36:02 2013 +0200
@@ -94,9 +94,84 @@
 Code_Target_Nat and Code_Target_Numeral.  See the tutorial on
 code generation for details.  INCOMPATIBILITY.
-* Theory "RealVector" and "Limits": Introduce type class
-(lin)order_topology. Allows to generalize theorems about limits and
-order. Instances are reals and extended reals.
+* Introduce type class "conditional_complete_lattice": Like a complete
+  lattice but does not assume the existence of the top and bottom elements.
+  Allows to generalize some lemmas about reals and extended reals.
+  Removed SupInf and replaced it by the instantiation of
+  conditional_complete_lattice for real. Renamed lemmas about conditional
+  complete lattice from Sup_... to cSup_... and from Inf_... to
+  cInf_... to avoid hidding of similar complete lattice lemmas.
+* 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.
+ - 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".
+   Generalized continuity lemmas from isCont to continuous on an arbitrary
+   filter.
+ - compact from Multivariate_Analysis. Use Bolzano's lemma
+   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, conditional complete linorder.
+ - 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.
+ - FDERIV: Definition of has_derivative moved to Deriv.thy. Moved theorems
+   from Library/FDERIV.thy to Deriv.thy and base the definition of DERIV on
+   FDERIV. Add variants of DERIV and FDERIV which are restricted to sets,
+   i.e. to represent derivatives from left or right.
+ - Removed the within-filter. It is replaced by the principal filter:
+     F within X = inf F (principal X)
+ - Introduce "at x within U" as a single constant, "at x" is now an
+   abbreviation for "at x within UNIV"
+ - Introduce named theorem collections tendsto_intros, continuous_intros,
+   continuous_on_intros and FDERIV_intros. Theorems in tendsto_intros (or
+   FDERIV_intros) are also available as tendsto_eq_intros (or
+   FDERIV_eq_intros) where the right-hand side is replaced by a congruence
+   rule. This allows to apply them as intro rules and then proving
+   equivalence by the simplifier.
+ - Restructured theories in HOL-Complex_Main:
+   + Moved RealDef and RComplete into Real
+   + Introduced Topological_Spaces and moved theorems about
+     topological spaces, filters, limits and continuity to it
+   + Renamed RealVector to Real_Vector_Spaces
+   + Split Lim, SEQ, Series into Topological_Spaces, Real_Vector_Spaces, and
+     Limits
+   + Moved Ln and Log to Transcendental
+   + Moved theorems about continuity from Deriv to Topological_Spaces
+ - Remove various auxiliary lemmas.
 * Consolidation of library theories on product orders: