# HG changeset patch
# User haftmann
# Date 1280135385 -7200
# Node ID 3e174df3f965214eae07da13b7d19d9451e8c107
# Parent  ac9bcae5ada746670fed9f089088dbe96e02765f
reactivated Scala check; tuned import order

diff -r ac9bcae5ada7 -r 3e174df3f965 src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Jul 26 11:09:45 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Jul 26 11:09:45 2010 +0200
@@ -5,7 +5,7 @@
 header {* An imperative in-place reversal on arrays *}
 
 theory Imperative_Reverse
-imports Imperative_HOL Subarray
+imports Subarray Imperative_HOL
 begin
 
 fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
@@ -110,6 +110,6 @@
       subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
   (drule sym[of "List.length (Array.get h a)"], simp)
 
-export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? (*Scala?*)
+export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
 
 end