isabelle: src/HOL/Imperative_HOL/Imperative_HOL_ex.thy@4c0a5e35931a (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
37771 1bec64044b5e spelt out relational framework in a consistent way haftmann parents: 36098 diff changeset	9	imports Imperative_HOL
1bec64044b5e spelt out relational framework in a consistent way haftmann parents: 36098 diff changeset	10	"ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker"
30694 4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	11	begin
4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	12
37826 4c0a5e35931a avoid export_code ... file - haftmann parents: 37771 diff changeset	13	export_code "Array." "Ref." checking SML SML_imp OCaml? OCaml_imp? Haskell?
4c0a5e35931a avoid export_code ... file - haftmann parents: 37771 diff changeset	14
30694 4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	15	end

author	haftmann
	Wed, 14 Jul 2010 16:13:14 +0200
changeset 37826	4c0a5e35931a
parent 37771	1bec64044b5e
child 37829	11f813e86305
permissions	-rw-r--r--