--- a/NEWS Mon Mar 09 16:28:19 2015 +0000
+++ b/NEWS Mon Mar 09 16:42:18 2015 +0000
@@ -73,6 +73,10 @@
*** HOL ***
+* 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.
+
* 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
--- a/src/HOL/HOLCF/Universal.thy Mon Mar 09 16:28:19 2015 +0000
+++ b/src/HOL/HOLCF/Universal.thy Mon Mar 09 16:42:18 2015 +0000
@@ -325,6 +325,8 @@
qed
qed
+no_notation binomial (infixl "choose" 65)
+
definition
choose :: "'a compact_basis set \<Rightarrow> 'a compact_basis"
where