1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Jul 26 11:09:45 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Jul 26 11:09:45 2010 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* An imperative in-place reversal on arrays *}
     1.5  
     1.6  theory Imperative_Reverse
     1.7 -imports Imperative_HOL Subarray
     1.8 +imports Subarray Imperative_HOL
     1.9  begin
    1.10  
    1.11  fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
    1.12 @@ -110,6 +110,6 @@
    1.13        subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
    1.14    (drule sym[of "List.length (Array.get h a)"], simp)
    1.15  
    1.16 -export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? (*Scala?*)
    1.17 +export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
    1.18  
    1.19  end