# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1425919338 0
# Node ID 1ce77bca58f864415a86f9415a9455530c8738d0
# Parent  0cc388370041c33c2dc8bd0de2982e956d89cb1d
Removed the infix operator "choose" to allow HOLCF to build

diff -r 0cc388370041 -r 1ce77bca58f8 NEWS
--- 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
diff -r 0cc388370041 -r 1ce77bca58f8 src/HOL/HOLCF/Universal.thy
--- 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