NEWS
changeset 23116 16e1401afe91
parent 23104 0a47a5681704
child 23129 a318773dca05
equal deleted 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):