src/HOL/Real_Vector_Spaces.thy
changeset 57418 6ab1c7cb0b8d
parent 57276 49c51eeaa623
child 57448 159e45728ceb
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Fri Jun 27 22:08:55 2014 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Sat Jun 28 09:16:42 2014 +0200
     1.3 @@ -450,7 +450,7 @@
     1.4      by (induct s rule: finite_induct) auto
     1.5  next
     1.6    case False then show ?thesis using assms
     1.7 -    by (metis Reals_0 setsum_infinite)
     1.8 +    by (metis Reals_0 setsum.infinite)
     1.9  qed
    1.10  
    1.11  lemma setprod_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
    1.12 @@ -459,7 +459,7 @@
    1.13      by (induct s rule: finite_induct) auto
    1.14  next
    1.15    case False then show ?thesis using assms
    1.16 -    by (metis Reals_1 setprod_infinite)
    1.17 +    by (metis Reals_1 setprod.infinite)
    1.18  qed
    1.19  
    1.20  lemma Reals_induct [case_names of_real, induct set: Reals]: