src/HOL/Lim.thy

 
 lemma (in bounded_bilinear) LIM_right_zero:
   "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
   by (rule tendsto_right_zero)
 
-lemmas LIM_mult = mult.LIM
-
-lemmas LIM_mult_zero = mult.LIM_prod_zero
-
-lemmas LIM_mult_left_zero = mult.LIM_left_zero
-
-lemmas LIM_mult_right_zero = mult.LIM_right_zero
-
-lemmas LIM_scaleR = scaleR.LIM
-
-lemmas LIM_of_real = of_real.LIM
+lemmas LIM_mult =
+  bounded_bilinear.LIM [OF bounded_bilinear_mult]
+
+lemmas LIM_mult_zero =
+  bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult]
+
+lemmas LIM_mult_left_zero =
+  bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult]
+
+lemmas LIM_mult_right_zero =
+  bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult]
+
+lemmas LIM_scaleR =
+  bounded_bilinear.LIM [OF bounded_bilinear_scaleR]
+
+lemmas LIM_of_real =
+  bounded_linear.LIM [OF bounded_linear_of_real]
 
 lemma LIM_power:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   assumes f: "f -- a --> l"
   shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"

 
 lemma (in bounded_bilinear) isCont:
   "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
   unfolding isCont_def by (rule LIM)
 
-lemmas isCont_scaleR [simp] = scaleR.isCont
-
-lemma isCont_of_real [simp]:
-  "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
-  by (rule of_real.isCont)
+lemmas isCont_scaleR [simp] =
+  bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
+
+lemmas isCont_of_real [simp] =
+  bounded_linear.isCont [OF bounded_linear_of_real]
 
 lemma isCont_power [simp]:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   unfolding isCont_def by (rule LIM_power)