isabelle: src/HOL/Library/Imperative_HOL.thy@e90d9d51106b (annotated)

26170 66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	1	(* Title: HOL/Library/Imperative_HOL.thy
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	2	ID: $Id$
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	3	Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	4	*)
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	5
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	6	header {* Entry point into monadic imperative HOL *}
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	7
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	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 66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	10	begin
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	11
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	12	end