src/HOL/UNITY/Comp/AllocImpl.thy
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