changeset 59659 | 1ce77bca58f8 |
parent 59648 | d1148f0baef5 |
child 59661 | c3b76f2bafbd |
--- a/NEWS Mon Mar 09 16:28:19 2015 +0000 +++ b/NEWS Mon Mar 09 16:42:18 2015 +0000 @@ -73,6 +73,10 @@ *** HOL *** +* the functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}" + type, so in particular on "real" and "complex" uniformly. + Minor INCOMPATIBILITY: type constraints may be needed. + * removed functions "natfloor" and "natceiling", use "nat o floor" and "nat o ceiling" instead. A few of the lemmas have been retained and adapted: in their names