--- a/src/HOL/Imperative_HOL/Heap.thy Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/Imperative_HOL/Heap.thy Thu Nov 12 17:21:48 2009 +0100
@@ -231,7 +231,7 @@
the literature? *}
lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
- by (simp add: get_array_def set_array_def)
+ by (simp add: get_array_def set_array_def o_def)
lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
by (simp add: noteq_arrs_def get_array_def set_array_def)