author | bulwahn |
Sat, 19 Jul 2008 19:27:13 +0200 | |
changeset 27656 | d4f6e64ee7cc |
parent 26170 | 66e6b967ccf1 |
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 |