author | wenzelm |
Sun, 02 Nov 2014 18:21:45 +0100 | |
changeset 58889 | 5b7a9633cfa8 |
parent 53109 | 186535065f5c |
child 61119 | 7beed856816c |
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 |
||
58889 | 6 |
section {* Monadic imperative HOL with examples *} |
30694 | 7 |
|
8 |
theory Imperative_HOL_ex |
|
39307 | 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 | 12 |
begin |
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 | 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 | 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 | 19 |
|
30694 | 20 |
end |