| changeset 50630 | 1ea90e8046dc |
| parent 39307 | 8d42d668b5b0 |
| child 53109 | 186535065f5c |
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Fri Dec 28 10:15:39 2012 +0100 +++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Fri Dec 28 10:25:59 2012 +0100 @@ -14,6 +14,6 @@ Array.upd, Array.map_entry, Array.swap, Array.freeze, ref, Ref.lookup, Ref.update, Ref.change)" -export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp? +export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp end