NEWS
 changeset 50526 899c9c4e4a4c parent 50525 46be26e02456 child 50592 a39250169636
1.1 --- a/NEWS	Fri Dec 14 14:46:01 2012 +0100
1.2 +++ b/NEWS	Fri Dec 14 15:46:01 2012 +0100
1.3 @@ -227,6 +227,36 @@
1.4  * HOL/Cardinals: Theories of ordinals and cardinals
1.5  (supersedes the AFP entry "Ordinals_and_Cardinals").
1.7 +* HOL/Multivariate_Analysis:
1.8 +  Replaced "basis :: 'a::euclidean_space => nat => real" and
1.9 +  "\<Chi>\<Chi> :: (nat => real) => 'a::euclidean_space" on euclidean spaces by
1.10 +  using the inner product "_ \<bullet> _" with vectors from the Basis set.
1.11 +  "\<Chi>\<Chi> i. f i" is replaced by "SUM i : Basis. f i *r i".
1.12 +
1.13 +  With this change the following constants are also chanegd or removed:
1.14 +
1.15 +    DIM('a) :: nat   ~>   card (Basis :: 'a set)   (is an abbreviation)
1.16 +    a \$\$ i    ~>    inner a i  (where i : Basis)
1.17 +    cart_base i     removed
1.18 +    \<pi>, \<pi>'   removed
1.19 +
1.20 +  Theorems about these constants where removed.
1.21 +
1.22 +  Renamed lemmas:
1.23 +
1.24 +    component_le_norm   ~>   Basis_le_norm
1.25 +    euclidean_eq   ~>   euclidean_eq_iff
1.26 +    differential_zero_maxmin_component   ~>   differential_zero_maxmin_cart
1.27 +    euclidean_simps   ~>   inner_simps
1.28 +    independent_basis   ~>   independent_Basis
1.29 +    span_basis   ~>   span_Basis
1.30 +    in_span_basis   ~>   in_span_Basis
1.31 +    norm_bound_component_le   ~>   norm_boound_Basis_le
1.32 +    norm_bound_component_lt   ~>   norm_boound_Basis_lt
1.33 +    component_le_infnorm   ~>   Basis_le_infnorm
1.34 +
1.35 +  INCOMPATIBILITY.
1.36 +
1.37  * HOL/Probability:
1.38    - Add simproc "measurable" to automatically prove measurability