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
10
begin
11
12
end