equal
deleted
inserted
replaced
6 header {* Combinators syntax for generic, open state monads (single threaded monads) *} |
6 header {* Combinators syntax for generic, open state monads (single threaded monads) *} |
7 |
7 |
8 theory State_Monad |
8 theory State_Monad |
9 imports Main |
9 imports Main |
10 begin |
10 begin |
11 |
|
12 section {* Generic, open state monads *} |
|
13 |
11 |
14 subsection {* Motivation *} |
12 subsection {* Motivation *} |
15 |
13 |
16 text {* |
14 text {* |
17 The logic HOL has no notion of constructor classes, so |
15 The logic HOL has no notion of constructor classes, so |