isabelle: src/HOL/Imperative_HOL/Imperative_HOL_ex.thy@d1ef88d7de5a (annotated)

30694 4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	1	(* Title: HOL/Imperative_HOL/Imperative_HOL_ex.thy
31872 a564aca741f2 tuned haftmann parents: 30694 diff changeset	2	Author: John Matthews, Galois Connections;
a564aca741f2 tuned haftmann parents: 30694 diff changeset	3	Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
30694 4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	4	*)
4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	5
31872 a564aca741f2 tuned haftmann parents: 30694 diff changeset	6	header {* Monadic imperative HOL with examples *}
30694 4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	7
4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	8	theory Imperative_HOL_ex
34051 1a82e2e29d67 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas bulwahn parents: 31872 diff changeset	9	imports Imperative_HOL "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists"
30694 4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	10	begin
4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	11
4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	12	end