(* Title: HOL/Imperative_HOL/Heap_Monad.thy Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen *) section ‹A monad with a polymorphic heap and primitive reasoning infrastructure› theory Heap_Monad imports Heap "HOL-Library.Monad_Syntax" begin subsection ‹The monad› subsubsection ‹Monad construction› text ‹Monadic heap actions either produce values and transform the heap, or fail›