# HG changeset patch
# User huffman
# Date 1292095597 28800
# Node ID b497cc48e5638498bb5ad4ec1a1fe358bb2977a6
# Parent  32099ee71a2fcd44402ac82736b036022cb0e69b
xsymbol notation for powerdomain types

diff -r 32099ee71a2f -r b497cc48e563 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Sat Dec 11 10:35:40 2010 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy	Sat Dec 11 11:26:37 2010 -0800
@@ -123,6 +123,8 @@
   "{S::'a pd_basis set. convex_le.ideal S}"
 by (rule convex_le.ex_ideal)
 
+type_notation (xsymbols) convex_pd ("('(_')\<natural>)")
+
 instantiation convex_pd :: ("domain") below
 begin
 
diff -r 32099ee71a2f -r b497cc48e563 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Sat Dec 11 10:35:40 2010 -0800
+++ b/src/HOL/HOLCF/LowerPD.thy	Sat Dec 11 11:26:37 2010 -0800
@@ -78,6 +78,8 @@
   "{S::'a pd_basis set. lower_le.ideal S}"
 by (rule lower_le.ex_ideal)
 
+type_notation (xsymbols) lower_pd ("('(_')\<flat>)")
+
 instantiation lower_pd :: ("domain") below
 begin
 
diff -r 32099ee71a2f -r b497cc48e563 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Sat Dec 11 10:35:40 2010 -0800
+++ b/src/HOL/HOLCF/UpperPD.thy	Sat Dec 11 11:26:37 2010 -0800
@@ -76,6 +76,8 @@
   "{S::'a pd_basis set. upper_le.ideal S}"
 by (rule upper_le.ex_ideal)
 
+type_notation (xsymbols) upper_pd ("('(_')\<sharp>)")
+
 instantiation upper_pd :: ("domain") below
 begin