| changeset 29400 | a462459fb5ce |
| parent 29398 | 89813bbf0f3e |
| parent 29399 | ebcd69a00872 |
| child 29413 | 43a12fc76f48 |
| child 29439 | 83601bdadae8 |
| child 29682 | 7bae3abff5d7 |
| 29398:89813bbf0f3e | 29400:a462459fb5ce |
|---|---|
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 |