| changeset 29822 | c45845743f04 |
| parent 29399 | ebcd69a00872 |
| child 37772 | 026ed2fc15d4 |
| 29819:7e4161257c9a | 29822:c45845743f04 |
|---|---|
1 (* Title: HOL/Library/Imperative_HOL.thy |
1 (* Title: HOL/Imperative_HOL/Imperative_HOL.thy |
2 ID: $Id$ |
|
3 Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
2 Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
4 *) |
3 *) |
5 |
4 |
6 header {* Entry point into monadic imperative HOL *} |
5 header {* Entry point into monadic imperative HOL *} |
7 |
6 |