src/HOL/Imperative_HOL/ex/Subarray.thy

--- a/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -68,4 +68,4 @@
 lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length h a \<longrightarrow> P (Array.get h a ! k))"
 unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
 
-end
\ No newline at end of file
+end