author | haftmann |
Wed, 14 Jul 2010 16:45:30 +0200 | |
changeset 37829 | 11f813e86305 |
parent 37826 | 4c0a5e35931a |
child 37831 | fa3a2e35c4f1 |
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 |
||
37829 | 13 |
definition "everything = (Array.new, Array.of_list, (*Array.make,*) Array.len, Array.nth, |
14 |
Array.upd, Array.map_entry, Array.swap, Array.freeze, |
|
15 |
ref, Ref.lookup, Ref.update(*, Ref.change*))" |
|
16 |
||
17 |
export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? |
|
37826 | 18 |
|
30694 | 19 |
end |