isabelle: src/HOL/Imperative_HOL/Imperative_HOL.thy@27c7b620758c (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

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Mon, 30 Aug 2010 15:44:33 +0900
changeset 38861	27c7b620758c
parent 37776	df0350f1e7f2
child 53109	186535065f5c
permissions	-rw-r--r--