isabelle: src/HOL/Imperative_HOL/Imperative_HOL_ex.thy@246985c6b20b (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
39307 8d42d668b5b0 added Imperative HOL overview haftmann parents: 38058 diff changeset	9	imports Imperative_HOL Overview
37771 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"
53109 186535065f5c renamed theory Mrec to Legacy_Mrec, no longer included by default krauss parents: 50630 diff changeset	11	Legacy_Mrec
30694 4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	12	begin
4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	13
37831 fa3a2e35c4f1 repaired some implementations of imperative operations haftmann parents: 37829 diff changeset	14	definition "everything = (Array.new, Array.of_list, Array.make, Array.len, Array.nth,
37829 11f813e86305 part of pervasive test haftmann parents: 37826 diff changeset	15	Array.upd, Array.map_entry, Array.swap, Array.freeze,
37831 fa3a2e35c4f1 repaired some implementations of imperative operations haftmann parents: 37829 diff changeset	16	ref, Ref.lookup, Ref.update, Ref.change)"
37829 11f813e86305 part of pervasive test haftmann parents: 37826 diff changeset	17
50630 1ea90e8046dc code checking for Scala is mandatory, since Scala is now required anyway for Isabelle haftmann parents: 39307 diff changeset	18	export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
37826 4c0a5e35931a avoid export_code ... file - haftmann parents: 37771 diff changeset	19
30694 4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	20	end

author	blanchet
	Wed, 24 Sep 2014 15:45:55 +0200
changeset 58425	246985c6b20b
parent 53109	186535065f5c
child 58889	5b7a9633cfa8
permissions	-rw-r--r--