diff -r 5eb932e604a2 -r eab6ce8368fa src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Library/State_Monad.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -140,10 +140,10 @@
 by (induction xs) auto
 
 abbreviation mono_state :: "('s::preorder, 'a) state \<Rightarrow> bool" where
-"mono_state \<equiv> state_io_rel (op \<le>)"
+"mono_state \<equiv> state_io_rel (\<le>)"
 
 abbreviation strict_mono_state :: "('s::preorder, 'a) state \<Rightarrow> bool" where
-"strict_mono_state \<equiv> state_io_rel (op <)"
+"strict_mono_state \<equiv> state_io_rel (<)"
 
 corollary strict_mono_implies_mono: "strict_mono_state m \<Longrightarrow> mono_state m"
 unfolding state_io_rel_def
@@ -230,4 +230,4 @@
 
 end
 
-end
\ No newline at end of file
+end