| changeset 29399 | ebcd69a00872 |
| parent 29397 | aab26a65e80f |
| child 29400 | a462459fb5ce |
| 29397:aab26a65e80f | 29399:ebcd69a00872 |
|---|---|
1 (* Title: HOL/Library/Imperative_HOL.thy |
|
2 ID: $Id$ |
|
3 Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Entry point into monadic imperative HOL *} |
|
7 |
|
8 theory Imperative_HOL |
|
9 imports Array Ref Relational |
|
10 begin |
|
11 |
|
12 end |