author | wenzelm |
Sat, 28 Jul 2012 20:36:25 +0200 | |
changeset 48589 | fb446a780d50 |
parent 37776 | df0350f1e7f2 |
child 53109 | 186535065f5c |
permissions | -rw-r--r-- |
29822 | 1 |
(* Title: HOL/Imperative_HOL/Imperative_HOL.thy |
26170 | 2 |
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Entry point into monadic imperative HOL *} |
|
6 |
||
7 |
theory Imperative_HOL |
|
37776 | 8 |
imports Array Ref Mrec |
26170 | 9 |
begin |
10 |
||
11 |
end |