| 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