isabelle: src/HOL/Imperative_HOL/Imperative_HOL.thy@026ed2fc15d4 (annotated)

29822 c45845743f04 authentic syntax for List.nth haftmann parents: 29399 diff changeset	1	(* Title: HOL/Imperative_HOL/Imperative_HOL.thy
26170 66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	2	Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	3	*)
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	4
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	5	header {* Entry point into monadic imperative HOL *}
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	6
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	7	theory Imperative_HOL
37772 026ed2fc15d4 split off mrec into separate theory haftmann parents: 29822 diff changeset	8	imports Array Ref Relational Mrec
26170 66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	9	begin
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	10
66e6b967ccf1 added theories for imperative HOL haftmann parents: diff changeset	11	end