equal
deleted
inserted
replaced
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? |
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? |
14 |
18 |
15 end |
19 end |