equal
deleted
inserted
replaced
77 *** HOL *** |
77 *** HOL *** |
78 |
78 |
79 * the functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}" |
79 * the functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}" |
80 type, so in particular on "real" and "complex" uniformly. |
80 type, so in particular on "real" and "complex" uniformly. |
81 Minor INCOMPATIBILITY: type constraints may be needed. |
81 Minor INCOMPATIBILITY: type constraints may be needed. |
|
82 |
|
83 * The factorial function, "fact", now has type "nat => 'a" (of a sort that admits |
|
84 numeric types including nat, int, real and complex. INCOMPATIBILITY: |
|
85 an expression such as "fact 3 = 6" may require a type constraint, and the combination |
|
86 "real (fact k)" is likely to be unsatisfactory. If a type conversion is still necessary, |
|
87 then use "of_nat (fact k)". |
82 |
88 |
83 * removed functions "natfloor" and "natceiling", |
89 * removed functions "natfloor" and "natceiling", |
84 use "nat o floor" and "nat o ceiling" instead. |
90 use "nat o floor" and "nat o ceiling" instead. |
85 A few of the lemmas have been retained and adapted: in their names |
91 A few of the lemmas have been retained and adapted: in their names |
86 "natfloor"/"natceiling" has been replaced by "nat_floor"/"nat_ceiling". |
92 "natfloor"/"natceiling" has been replaced by "nat_floor"/"nat_ceiling". |