isabelle: src/HOL/Imperative_HOL/Imperative_HOL.thy@fa3a2e35c4f1 (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
37776 df0350f1e7f2 dropped empty theory haftmann parents: 37772 diff changeset	8	imports Array Ref 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