author | haftmann |
Wed, 14 Jul 2010 17:15:58 +0200 | |
changeset 37831 | fa3a2e35c4f1 |
parent 37829 | 11f813e86305 |
child 37845 | b70d7a347964 |
permissions | -rw-r--r-- |
30694 | 1 |
(* Title: HOL/Imperative_HOL/Imperative_HOL_ex.thy |
31872 | 2 |
Author: John Matthews, Galois Connections; |
3 |
Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
|
30694 | 4 |
*) |
5 |
||
31872 | 6 |
header {* Monadic imperative HOL with examples *} |
30694 | 7 |
|
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 | 11 |
begin |
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 | 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 | 16 |
|
17 |
export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? |
|
37826 | 18 |
|
30694 | 19 |
end |