| changeset 61954 | 1d43f86f48be |
| parent 60773 | d09c66a0ea10 |
| child 63146 | f1ecba0272f9 |
--- a/src/HOL/UNITY/Comp/AllocImpl.thy Mon Dec 28 18:03:26 2015 +0100 +++ b/src/HOL/UNITY/Comp/AllocImpl.thy Mon Dec 28 19:23:15 2015 +0100 @@ -375,7 +375,7 @@ lemma alloc_refinement_lemma: "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s}) - \<subseteq> {s. (SUM x: lessThan n. f x) \<le> (SUM x: lessThan n. g x s)}" + \<subseteq> {s. (\<Sum>x \<in> lessThan n. f x) \<le> (\<Sum>x \<in> lessThan n. g x s)}" apply (induct_tac "n") apply (auto simp add: lessThan_Suc) done