--- a/src/HOL/Real_Vector_Spaces.thy Tue Mar 17 17:45:03 2015 +0000
+++ b/src/HOL/Real_Vector_Spaces.thy Wed Mar 18 14:13:27 2015 +0000
@@ -444,7 +444,8 @@
then show thesis ..
qed
-lemma setsum_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
+lemma setsum_in_Reals [intro,simp]:
+ assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
proof (cases "finite s")
case True then show ?thesis using assms
by (induct s rule: finite_induct) auto
@@ -453,7 +454,8 @@
by (metis Reals_0 setsum.infinite)
qed
-lemma setprod_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
+lemma setprod_in_Reals [intro,simp]:
+ assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
proof (cases "finite s")
case True then show ?thesis using assms
by (induct s rule: finite_induct) auto