src/HOL/HOLCF/Pcpo.thy

--- a/src/HOL/HOLCF/Pcpo.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/Pcpo.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -143,12 +143,9 @@
   assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
 begin
 
-definition bottom :: "'a"
+definition bottom :: "'a"  ("\<bottom>")
   where "bottom = (THE x. \<forall>y. x \<sqsubseteq> y)"
 
-notation (xsymbols)
-  bottom ("\<bottom>")
-
 lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
 unfolding bottom_def
 apply (rule the1I2)