src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 81995 d67dadd69d07
parent 81706 7beb0cf38292
child 82447 741f6f6df144
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jan 27 21:31:02 2025 +0100
@@ -250,7 +250,7 @@
                 | None \<Rightarrow> None)"
 
 adhoc_overloading
-  Monad_Syntax.bind Heap_Monad.bind
+  Monad_Syntax.bind \<rightleftharpoons> Heap_Monad.bind
 
 lemma execute_bind [execute_simps]:
   "execute f h = Some (x, h') \<Longrightarrow> execute (f \<bind> g) h = execute (g x) h'"