--- a/src/HOL/Imperative_HOL/ex/Subarray.thy Sun Sep 30 07:46:38 2018 +0200
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy Sun Sep 30 09:00:11 2018 +0200
@@ -23,7 +23,7 @@
apply simp
done
-lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h[i - n := v]"
+lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.update a i v h) = (subarray n m a h)[i - n := v]"
unfolding subarray_def Array.update_def
by (simp add: nths'_update3)