--- a/NEWS Tue Mar 10 16:12:35 2015 +0000
+++ b/NEWS Mon Mar 16 15:30:00 2015 +0000
@@ -80,6 +80,12 @@
type, so in particular on "real" and "complex" uniformly.
Minor INCOMPATIBILITY: type constraints may be needed.
+* 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)".
+
* 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