isabelle: src/HOL/Imperative_HOL/Imperative_HOL.thy@25c0d4c0e110 (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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	5	section \<open>Entry point into monadic imperative HOL\<close>
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