src/HOL/Library/Imperative_HOL.thy
author haftmann
Mon Jul 07 08:47:17 2008 +0200 (2008-07-07)
changeset 27487 c8a6ce181805
parent 26170 66e6b967ccf1
child 27656 d4f6e64ee7cc
permissions -rw-r--r--
absolute imports of HOL/*.thy theories
haftmann@26170
     1
(*  Title:      HOL/Library/Imperative_HOL.thy
haftmann@26170
     2
    ID:         $Id$
haftmann@26170
     3
    Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
haftmann@26170
     4
*)
haftmann@26170
     5
haftmann@26170
     6
header {* Entry point into monadic imperative HOL *}
haftmann@26170
     7
haftmann@26170
     8
theory Imperative_HOL
haftmann@26170
     9
imports Array Ref
haftmann@26170
    10
begin
haftmann@26170
    11
haftmann@26170
    12
end