--- a/src/HOL/Algebra/Order.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Algebra/Order.thy Wed Jan 10 15:25:09 2018 +0100
@@ -22,7 +22,7 @@
abbreviation inv_gorder :: "_ \<Rightarrow> 'a gorder" where
"inv_gorder L \<equiv>
\<lparr> carrier = carrier L,
- eq = op .=\<^bsub>L\<^esub>,
+ eq = (.=\<^bsub>L\<^esub>),
le = (\<lambda> x y. y \<sqsubseteq>\<^bsub>L \<^esub>x) \<rparr>"
lemma inv_gorder_inv:
@@ -591,7 +591,7 @@
subsection \<open>Partial orders where \<open>eq\<close> is the Equality\<close>
locale partial_order = weak_partial_order +
- assumes eq_is_equal: "op .= = op ="
+ assumes eq_is_equal: "(.=) = (=)"
begin
declare weak_le_antisym [rule del]