--- a/NEWS Thu Mar 19 11:54:20 2015 +0100
+++ b/NEWS Thu Mar 19 14:24:51 2015 +0000
@@ -83,14 +83,14 @@
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,
+* New library of properties of the complex transcendental functions sin, cos, tan, 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
"real (fact k)" is likely to be unsatisfactory. If a type conversion is still necessary,
- then use "of_nat (fact k)".
+ then use "of_nat (fact k)" or "real_of_nat (fact k)".
* removed functions "natfloor" and "natceiling",
use "nat o floor" and "nat o ceiling" instead.