Renamed some bound variables due to changes in simplifier.
authorberghofe
Mon, 12 Nov 2001 10:43:25 +0100
changeset 12154 3a7fe282af9d
parent 12153 dc67fdb03a2a
child 12155 13c5469b4bb3
Renamed some bound variables due to changes in simplifier.
src/HOL/UNITY/Comp/AllocImpl.ML
--- a/src/HOL/UNITY/Comp/AllocImpl.ML	Mon Nov 12 10:39:42 2001 +0100
+++ b/src/HOL/UNITY/Comp/AllocImpl.ML	Mon Nov 12 10:43:25 2001 +0100
@@ -150,7 +150,7 @@
 
 
 Goal "!!f::nat=>nat. (INT i: lessThan n. {s. f i <= g i s})  \
-\     <= {s. (\\<Sum>i: lessThan n. f i) <= (\\<Sum>i: lessThan n. g i s)}";
+\     <= {s. (\\<Sum>x: lessThan n. f x) <= (\\<Sum>x: lessThan n. g x s)}";
 by (induct_tac "n" 1);
 by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
 qed "alloc_refinement_lemma";