isabelle: src/HOL/Imperative_HOL/Imperative_HOL_ex.thy@35815ce9218a (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"
36098 53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile bulwahn parents: 34051 diff changeset	10	"ex/SatChecker"
30694 4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	11	begin
4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	12
4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	13	end

author	wenzelm
	Mon, 21 Jun 2010 11:24:19 +0200
changeset 37380	35815ce9218a
parent 36098	53992c639da5
child 37771	1bec64044b5e
permissions	-rw-r--r--