src/HOL/HOLCF/LowerPD.thy
changeset 41111 b497cc48e563
parent 41110 32099ee71a2f
child 41284 6d66975b711f
--- 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