--- a/src/HOL/ex/Summation.thy Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/ex/Summation.thy Tue Sep 07 10:05:19 2010 +0200
@@ -24,7 +24,7 @@
lemma \<Delta>_shift:
"\<Delta> (\<lambda>k. l + f k) = \<Delta> f"
- by (simp add: \<Delta>_def expand_fun_eq)
+ by (simp add: \<Delta>_def ext_iff)
lemma \<Delta>_same_shift:
assumes "\<Delta> f = \<Delta> g"
@@ -100,7 +100,7 @@
proof -
from \<Delta>_\<Sigma> have "\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f" .
then obtain k where "plus k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
- then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: expand_fun_eq)
+ then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: ext_iff)
then show ?thesis by simp
qed