author | haftmann |
Wed, 21 Jan 2009 16:47:31 +0100 | |
changeset 29580 | 117b88da143c |
parent 29399 | ebcd69a00872 |
child 29822 | c45845743f04 |
permissions | -rw-r--r-- |
26170 | 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 |
|
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26170
diff
changeset
|
9 |
imports Array Ref Relational |
26170 | 10 |
begin |
11 |
||
12 |
end |