src/HOL/Lim.thy
changeset 44282 f0de18b62d63
parent 44254 336dd390e4a4
child 44310 ba3d031b5dbb
     1.1 --- a/src/HOL/Lim.thy	Thu Aug 18 17:42:35 2011 +0200
     1.2 +++ b/src/HOL/Lim.thy	Thu Aug 18 13:36:58 2011 -0700
     1.3 @@ -321,17 +321,23 @@
     1.4    "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
     1.5    by (rule tendsto_right_zero)
     1.6  
     1.7 -lemmas LIM_mult = mult.LIM
     1.8 +lemmas LIM_mult =
     1.9 +  bounded_bilinear.LIM [OF bounded_bilinear_mult]
    1.10  
    1.11 -lemmas LIM_mult_zero = mult.LIM_prod_zero
    1.12 +lemmas LIM_mult_zero =
    1.13 +  bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult]
    1.14  
    1.15 -lemmas LIM_mult_left_zero = mult.LIM_left_zero
    1.16 +lemmas LIM_mult_left_zero =
    1.17 +  bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult]
    1.18  
    1.19 -lemmas LIM_mult_right_zero = mult.LIM_right_zero
    1.20 +lemmas LIM_mult_right_zero =
    1.21 +  bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult]
    1.22  
    1.23 -lemmas LIM_scaleR = scaleR.LIM
    1.24 +lemmas LIM_scaleR =
    1.25 +  bounded_bilinear.LIM [OF bounded_bilinear_scaleR]
    1.26  
    1.27 -lemmas LIM_of_real = of_real.LIM
    1.28 +lemmas LIM_of_real =
    1.29 +  bounded_linear.LIM [OF bounded_linear_of_real]
    1.30  
    1.31  lemma LIM_power:
    1.32    fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
    1.33 @@ -446,11 +452,11 @@
    1.34    "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
    1.35    unfolding isCont_def by (rule LIM)
    1.36  
    1.37 -lemmas isCont_scaleR [simp] = scaleR.isCont
    1.38 +lemmas isCont_scaleR [simp] =
    1.39 +  bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
    1.40  
    1.41 -lemma isCont_of_real [simp]:
    1.42 -  "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
    1.43 -  by (rule of_real.isCont)
    1.44 +lemmas isCont_of_real [simp] =
    1.45 +  bounded_linear.isCont [OF bounded_linear_of_real]
    1.46  
    1.47  lemma isCont_power [simp]:
    1.48    fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"