NEWS
 changeset 23116 16e1401afe91 parent 23104 0a47a5681704 child 23129 a318773dca05
equal inserted replaced
23115:4615b2078592 23116:16e1401afe91
`   922   (NS)Cauchy     :: (nat => 'a::real_normed_vector) => bool`
`   922   (NS)Cauchy     :: (nat => 'a::real_normed_vector) => bool`
`   923   (NS)LIM        :: ['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool`
`   923   (NS)LIM        :: ['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool`
`   924   is(NS)Cont     :: ['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool`
`   924   is(NS)Cont     :: ['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool`
`   925   deriv          :: ['a::real_normed_field => 'a, 'a, 'a] => bool`
`   925   deriv          :: ['a::real_normed_field => 'a, 'a, 'a] => bool`
`   926   sgn            :: 'a::real_normed_vector => 'a`
`   926   sgn            :: 'a::real_normed_vector => 'a`
`       `
`   927   exp            :: 'a::{recpower,real_normed_field,banach} => 'a`
`   927 `
`   928 `
`   928 * Complex: Some complex-specific constants are now abbreviations for`
`   929 * Complex: Some complex-specific constants are now abbreviations for`
`   929 overloaded ones: complex_of_real = of_real, cmod = norm, hcmod =`
`   930 overloaded ones: complex_of_real = of_real, cmod = norm, hcmod =`
`   930 hnorm.  Other constants have been entirely removed in favor of the`
`   931 hnorm.  Other constants have been entirely removed in favor of the`
`   931 polymorphic versions (INCOMPATIBILITY):`
`   932 polymorphic versions (INCOMPATIBILITY):`