author | wenzelm |
Sat, 07 Apr 2012 16:41:59 +0200 | |
changeset 47389 | e8552cba702d |
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 |