109 * The functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}" |
109 * The functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}" |
110 type, so in particular on "real" and "complex" uniformly. |
110 type, so in particular on "real" and "complex" uniformly. |
111 Minor INCOMPATIBILITY: type constraints may be needed. |
111 Minor INCOMPATIBILITY: type constraints may be needed. |
112 |
112 |
113 * New library of properties of the complex transcendental functions sin, cos, tan, exp, |
113 * New library of properties of the complex transcendental functions sin, cos, tan, exp, |
114 ported from HOL Light. |
114 Ln, Arctan, Arcsin, Arccos. Ported from HOL Light. |
115 |
115 |
116 * The factorial function, "fact", now has type "nat => 'a" (of a sort that admits |
116 * The factorial function, "fact", now has type "nat => 'a" (of a sort that admits |
117 numeric types including nat, int, real and complex. INCOMPATIBILITY: |
117 numeric types including nat, int, real and complex. INCOMPATIBILITY: |
118 an expression such as "fact 3 = 6" may require a type constraint, and the combination |
118 an expression such as "fact 3 = 6" may require a type constraint, and the combination |
119 "real (fact k)" is likely to be unsatisfactory. If a type conversion is still necessary, |
119 "real (fact k)" is likely to be unsatisfactory. If a type conversion is still necessary, |