src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 39307 8d42d668b5b0
child 50630 1ea90e8046dc
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
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@39307
     9
imports Imperative_HOL Overview
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@38058
    17
export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
haftmann@37826
    18
haftmann@30694
    19
end