isabelle: src/HOL/Imperative_HOL/Imperative_HOL_ex.thy@ac6f8fff036b (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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 61119 diff changeset	6	section \<open>Monadic imperative HOL with examples\<close>
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"
30694 4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	11	begin
4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	12
37831 fa3a2e35c4f1 repaired some implementations of imperative operations haftmann parents: 37829 diff changeset	13	definition "everything = (Array.new, Array.of_list, Array.make, Array.len, Array.nth,
37829 11f813e86305 part of pervasive test haftmann parents: 37826 diff changeset	14	Array.upd, Array.map_entry, Array.swap, Array.freeze,
37831 fa3a2e35c4f1 repaired some implementations of imperative operations haftmann parents: 37829 diff changeset	15	ref, Ref.lookup, Ref.update, Ref.change)"
37829 11f813e86305 part of pervasive test haftmann parents: 37826 diff changeset	16
50630 1ea90e8046dc code checking for Scala is mandatory, since Scala is now required anyway for Isabelle haftmann parents: 39307 diff changeset	17	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	18
30694 4b182a031731 added Imperative_HOL_ex haftmann parents: diff changeset	19	end

author	wenzelm
	Fri, 07 May 2021 13:17:29 +0200
changeset 73642	ac6f8fff036b
parent 63167	0909deb8059b
permissions	-rw-r--r--