# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1528730601 -3600
# Node ID e0b5f2d14bf9315769caf461a55ddd51803de6fe
# Parent  32f445237d36eb3cd616c23bded35c9c002fd89c
fixed a name clash

diff -r 32f445237d36 -r e0b5f2d14bf9 src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Mon Jun 11 15:53:22 2018 +0100
+++ b/src/HOL/Analysis/Infinite_Products.thy	Mon Jun 11 16:23:21 2018 +0100
@@ -1431,7 +1431,7 @@
 
 subsection\<open>Embeddings from the reals into some complete real normed field\<close>
 
-lemma tendsto_of_real:
+lemma tendsto_eq_of_real_lim:
   assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q"
   shows "q = of_real (lim f)"
 proof -
@@ -1444,10 +1444,10 @@
     by (metis LIMSEQ_unique assms convergentD sequentially_bot tendsto_Lim tendsto_of_real)
 qed
 
-lemma tendsto_of_real':
+lemma tendsto_eq_of_real:
   assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q"
   obtains r where "q = of_real r"
-  using tendsto_of_real assms by blast
+  using tendsto_eq_of_real_lim assms by blast
 
 lemma has_prod_of_real_iff:
   "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) has_prod of_real c \<longleftrightarrow> f has_prod c"
@@ -1456,7 +1456,7 @@
   assume ?lhs
   then show ?rhs
     apply (auto simp: prod_defs LIMSEQ_prod_0 tendsto_of_real_iff simp flip: of_real_prod)
-    using tendsto_of_real'
+    using tendsto_eq_of_real
     by (metis of_real_0 tendsto_of_real_iff)
 next
   assume ?rhs