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'"