NEWS
changeset 45774 1d5079a5a0a2
parent 45772 ed5ddf9fcc77
child 45775 2ba4174f1e7d
     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