author | haftmann |
Fri, 11 Jun 2010 17:14:02 +0200 | |
changeset 37407 | 61dd8c145da7 |
parent 29822 | c45845743f04 |
child 37772 | 026ed2fc15d4 |
permissions | -rw-r--r-- |
29822 | 1 |
(* Title: HOL/Imperative_HOL/Imperative_HOL.thy |
26170 | 2 |
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Entry point into monadic imperative HOL *} |
|
6 |
||
7 |
theory Imperative_HOL |
|
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26170
diff
changeset
|
8 |
imports Array Ref Relational |
26170 | 9 |
begin |
10 |
||
11 |
end |