src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
author haftmann
Fri Jul 23 10:58:13 2010 +0200 (2010-07-23)
changeset 37947 844977c7abeb
parent 37845 b70d7a347964
child 37959 6fe5fa827f18
permissions -rw-r--r--
avoid unreliable Haskell Int type
haftmann@30694
     1
(*  Title:      HOL/Imperative_HOL/Imperative_HOL_ex.thy
haftmann@31872
     2
    Author:     John Matthews, Galois Connections;
haftmann@31872
     3
                Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
haftmann@30694
     4
*)
haftmann@30694
     5
haftmann@31872
     6
header {* Monadic imperative HOL with examples *}
haftmann@30694
     7
haftmann@30694
     8
theory Imperative_HOL_ex
haftmann@37771
     9
imports Imperative_HOL
haftmann@37771
    10
  "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker"
haftmann@30694
    11
begin
haftmann@30694
    12
haftmann@37831
    13
definition "everything = (Array.new, Array.of_list, Array.make, Array.len, Array.nth,
haftmann@37829
    14
  Array.upd, Array.map_entry, Array.swap, Array.freeze,
haftmann@37831
    15
  ref, Ref.lookup, Ref.update, Ref.change)"
haftmann@37829
    16
haftmann@37845
    17
export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
haftmann@37826
    18
haftmann@30694
    19
end