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.6  
     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
    1.39