src/HOL/Library/Imperative_HOL.thy
author bulwahn
Sat Jul 19 19:27:13 2008 +0200 (2008-07-19)
changeset 27656 d4f6e64ee7cc
parent 26170 66e6b967ccf1
permissions -rw-r--r--
added verification framework for the HeapMonad and quicksort as example for this framework
     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 Relational
    10 begin
    11 
    12 end