1.1 --- a/NEWS Mon Sep 12 09:21:01 2011 -0700
1.2 +++ b/NEWS Mon Sep 12 09:37:49 2011 -0700
1.3 @@ -266,6 +266,12 @@
1.4 * Theory Limits: Type "'a net" has been renamed to "'a filter", in
1.5 accordance with standard mathematical terminology. INCOMPATIBILITY.
1.6
1.7 +* Session Multivariate_Analysis: The euclidean_space type class now
1.8 +fixes a constant "Basis :: 'a set" consisting of the standard
1.9 +orthonormal basis for the type. Users now have the option of
1.10 +quantifying over this set instead of using the "basis" function, e.g.
1.11 +"ALL x:Basis. P x" vs "ALL i<DIM('a). P (basis i)".
1.12 +
1.13 * Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed
1.14 to "('a, 'b) vec" (the syntax "'a ^ 'b" remains unaffected). Constants
1.15 "Cart_nth" and "Cart_lambda" have been respectively renamed to
1.16 @@ -414,9 +420,10 @@
1.17 LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at]
1.18
1.19 * Theory Complex_Main: The definition of infinite series was generalized.
1.20 - Now it is defined on the type class {topological_spaces, comm_monoid_add}.
1.21 + Now it is defined on the type class {topological_space, comm_monoid_add}.
1.22 Hence it is useable also for extended real numbers.
1.23
1.24 +
1.25 *** Document preparation ***
1.26
1.27 * Localized \isabellestyle switch can be used within blocks or groups