--- a/NEWS Wed Mar 18 14:55:17 2015 +0000
+++ b/NEWS Wed Mar 18 17:23:22 2015 +0000
@@ -79,10 +79,13 @@
* New proof method "rewrite" (in ~~/src/HOL/Library/Rewrite) for
single-step rewriting with subterm selection based on patterns.
-* the functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}"
+* 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.
+* New library of properties of the complex transcendental functions sin, cos, exp,
+ ported from HOL Light.
+
* The factorial function, "fact", now has type "nat => 'a" (of a sort that admits
numeric types including nat, int, real and complex. INCOMPATIBILITY:
an expression such as "fact 3 = 6" may require a type constraint, and the combination