haftmann@29822: (*  Title:      HOL/Imperative_HOL/Imperative_HOL.thy
haftmann@26170:     Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
haftmann@26170: *)
haftmann@26170: 
haftmann@26170: header {* Entry point into monadic imperative HOL *}
haftmann@26170: 
haftmann@26170: theory Imperative_HOL
haftmann@37776: imports Array Ref Mrec
haftmann@26170: begin
haftmann@26170: 
haftmann@26170: end