equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* A monad with a polymorphic heap and primitive reasoning infrastructure *} |
5 header {* A monad with a polymorphic heap and primitive reasoning infrastructure *} |
6 |
6 |
7 theory Heap_Monad |
7 theory Heap_Monad |
8 imports Heap Monad_Syntax Code_Natural |
8 imports |
|
9 Heap |
|
10 "~~/src/HOL/Library/Monad_Syntax" |
|
11 "~~/src/HOL/Library/Code_Natural" |
9 begin |
12 begin |
10 |
13 |
11 subsection {* The monad *} |
14 subsection {* The monad *} |
12 |
15 |
13 subsubsection {* Monad construction *} |
16 subsubsection {* Monad construction *} |