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: 
wenzelm@58889: section {* Entry point into monadic imperative HOL *}
haftmann@26170: 
haftmann@26170: theory Imperative_HOL
krauss@53109: imports Array Ref
haftmann@26170: begin
haftmann@26170: 
haftmann@26170: end