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
     1 (*  Title:      HOL/Imperative_HOL/Imperative_HOL_ex.thy
     2     Author:     John Matthews, Galois Connections;
     3                 Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
     4 *)
     5 
     6 header {* Monadic imperative HOL with examples *}
     7 
     8 theory Imperative_HOL_ex
     9 imports Imperative_HOL Overview
    10   "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker"
    11 begin
    12 
    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? Scala? Scala_imp?
    18 
    19 end