isabelle: src/HOL/Imperative_HOL/Imperative_HOL.thy@d3996d5873dd (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
58889 5b7a9633cfa8 modernized header uniformly as section; wenzelm parents: 53109 diff changeset	5	section {* Entry point into monadic imperative HOL *}
26170 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
53109 186535065f5c renamed theory Mrec to Legacy_Mrec, no longer included by default krauss parents: 37776 diff changeset	8	imports Array Ref
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