| changeset 37772 | 026ed2fc15d4 |
| parent 29822 | c45845743f04 |
| child 37776 | df0350f1e7f2 |
| 37771:1bec64044b5e | 37772:026ed2fc15d4 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Entry point into monadic imperative HOL *} |
5 header {* Entry point into monadic imperative HOL *} |
6 |
6 |
7 theory Imperative_HOL |
7 theory Imperative_HOL |
8 imports Array Ref Relational |
8 imports Array Ref Relational Mrec |
9 begin |
9 begin |
10 |
10 |
11 end |
11 end |