--- a/src/HOL/HOLCF/Up.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/HOLCF/Up.thy Wed Jan 10 15:25:09 2018 +0100
@@ -28,7 +28,7 @@
begin
definition below_up_def:
- "(op \<sqsubseteq>) \<equiv>
+ "(\<sqsubseteq>) \<equiv>
(\<lambda>x y.
(case x of
Ibottom \<Rightarrow> True