src/HOL/Library/Imperative_HOL.thy
author wenzelm
Thu Oct 16 22:44:24 2008 +0200 (2008-10-16)
changeset 28615 4c8fa015ec7f
parent 27656 d4f6e64ee7cc
permissions -rw-r--r--
explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
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
bulwahn@27656
     9
imports Array Ref Relational
haftmann@26170
    10
begin
haftmann@26170
    11
haftmann@26170
    12
end