| changeset 15074 | 277b3a4da341 |
| parent 14114 | e97ca1034caa |
| child 16417 | 9bc16273c2d4 |
--- a/src/HOL/UNITY/Comp/AllocImpl.thy Thu Jul 22 12:55:36 2004 +0200 +++ b/src/HOL/UNITY/Comp/AllocImpl.thy Thu Jul 22 17:37:31 2004 +0200 @@ -353,7 +353,7 @@ lemma alloc_refinement_lemma: "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s}) - \<subseteq> {s. (\<Sum>x \<in> lessThan n. f x) \<le> (\<Sum>x: lessThan n. g x s)}" + \<subseteq> {s. (SUM x: lessThan n. f x) \<le> (SUM x: lessThan n. g x s)}" apply (induct_tac "n") apply (auto simp add: lessThan_Suc) done