| changeset 27656 | d4f6e64ee7cc |
| parent 26170 | 66e6b967ccf1 |
| 27655:cf0c60e821bb | 27656:d4f6e64ee7cc |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Entry point into monadic imperative HOL *} |
6 header {* Entry point into monadic imperative HOL *} |
7 |
7 |
8 theory Imperative_HOL |
8 theory Imperative_HOL |
9 imports Array Ref |
9 imports Array Ref Relational |
10 begin |
10 begin |
11 |
11 |
12 end |
12 end |