src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
changeset 37826 4c0a5e35931a
parent 37771 1bec64044b5e
child 37829 11f813e86305
equal deleted inserted replaced
37825:adc1143bc1a8 37826:4c0a5e35931a
     8 theory Imperative_HOL_ex
     8 theory Imperative_HOL_ex
     9 imports Imperative_HOL
     9 imports Imperative_HOL
    10   "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker"
    10   "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker"
    11 begin
    11 begin
    12 
    12 
       
    13 export_code "Array.*" "Ref.*" checking SML SML_imp OCaml? OCaml_imp? Haskell?
       
    14 
    13 end
    15 end