changeset 29396 | ebcd69a00872 |
parent 27656 | d4f6e64ee7cc |
child 29759 | c45845743f04 |
1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 1.2 +++ b/src/HOL/Imperative_HOL/Imperative_HOL.thy Thu Jan 08 17:10:41 2009 +0100 1.3 @@ -0,0 +1,12 @@ 1.4 +(* Title: HOL/Library/Imperative_HOL.thy 1.5 + ID: $Id$ 1.6 + Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen 1.7 +*) 1.8 + 1.9 +header {* Entry point into monadic imperative HOL *} 1.10 + 1.11 +theory Imperative_HOL 1.12 +imports Array Ref Relational 1.13 +begin 1.14 + 1.15 +end