src/HOL/Library/State_Monad.thy
changeset 66258 2b83dd24b301
parent 63680 6e1e8b5abbfa
equal deleted inserted replaced
66257:3bc892346a6b 66258:2b83dd24b301
     3 *)
     3 *)
     4 
     4 
     5 section \<open>Combinator syntax for generic, open state monads (single-threaded monads)\<close>
     5 section \<open>Combinator syntax for generic, open state monads (single-threaded monads)\<close>
     6 
     6 
     7 theory State_Monad
     7 theory State_Monad
     8 imports Main Monad_Syntax
     8 imports Main
     9 begin
     9 begin
    10 
    10 
    11 subsection \<open>Motivation\<close>
    11 subsection \<open>Motivation\<close>
    12 
    12 
    13 text \<open>
    13 text \<open>