--- a/src/HOL/HOLCF/ConvexPD.thy Mon Dec 06 13:43:05 2010 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy Mon Dec 06 14:17:35 2010 -0800
@@ -342,6 +342,13 @@
convex_bind :: "'a convex_pd \<rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
"convex_bind = convex_pd.basis_fun convex_bind_basis"
+syntax
+ "_convex_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
+ ("(3\<Union>\<natural>_\<in>_./ _)" [0, 0, 10] 10)
+
+translations
+ "\<Union>\<natural>x\<in>xs. e" == "CONST convex_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
+
lemma convex_bind_principal [simp]:
"convex_bind\<cdot>(convex_principal t) = convex_bind_basis t"
unfolding convex_bind_def
--- a/src/HOL/HOLCF/LowerPD.thy Mon Dec 06 13:43:05 2010 -0800
+++ b/src/HOL/HOLCF/LowerPD.thy Mon Dec 06 14:17:35 2010 -0800
@@ -335,6 +335,13 @@
lower_bind :: "'a lower_pd \<rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where
"lower_bind = lower_pd.basis_fun lower_bind_basis"
+syntax
+ "_lower_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
+ ("(3\<Union>\<flat>_\<in>_./ _)" [0, 0, 10] 10)
+
+translations
+ "\<Union>\<flat>x\<in>xs. e" == "CONST lower_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
+
lemma lower_bind_principal [simp]:
"lower_bind\<cdot>(lower_principal t) = lower_bind_basis t"
unfolding lower_bind_def
--- a/src/HOL/HOLCF/UpperPD.thy Mon Dec 06 13:43:05 2010 -0800
+++ b/src/HOL/HOLCF/UpperPD.thy Mon Dec 06 14:17:35 2010 -0800
@@ -330,6 +330,13 @@
upper_bind :: "'a upper_pd \<rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
"upper_bind = upper_pd.basis_fun upper_bind_basis"
+syntax
+ "_upper_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
+ ("(3\<Union>\<sharp>_\<in>_./ _)" [0, 0, 10] 10)
+
+translations
+ "\<Union>\<sharp>x\<in>xs. e" == "CONST upper_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
+
lemma upper_bind_principal [simp]:
"upper_bind\<cdot>(upper_principal t) = upper_bind_basis t"
unfolding upper_bind_def