src/HOL/Lim.thy
changeset 44282 f0de18b62d63
parent 44254 336dd390e4a4
child 44310 ba3d031b5dbb
--- a/src/HOL/Lim.thy	Thu Aug 18 17:42:35 2011 +0200
+++ b/src/HOL/Lim.thy	Thu Aug 18 13:36:58 2011 -0700
@@ -321,17 +321,23 @@
   "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
   by (rule tendsto_right_zero)
 
-lemmas LIM_mult = mult.LIM
+lemmas LIM_mult =
+  bounded_bilinear.LIM [OF bounded_bilinear_mult]
 
-lemmas LIM_mult_zero = mult.LIM_prod_zero
+lemmas LIM_mult_zero =
+  bounded_bilinear.LIM_prod_zero [OF bounded_bilinear_mult]
 
-lemmas LIM_mult_left_zero = mult.LIM_left_zero
+lemmas LIM_mult_left_zero =
+  bounded_bilinear.LIM_left_zero [OF bounded_bilinear_mult]
 
-lemmas LIM_mult_right_zero = mult.LIM_right_zero
+lemmas LIM_mult_right_zero =
+  bounded_bilinear.LIM_right_zero [OF bounded_bilinear_mult]
 
-lemmas LIM_scaleR = scaleR.LIM
+lemmas LIM_scaleR =
+  bounded_bilinear.LIM [OF bounded_bilinear_scaleR]
 
-lemmas LIM_of_real = of_real.LIM
+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}"
@@ -446,11 +452,11 @@
   "\<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
+lemmas isCont_scaleR [simp] =
+  bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
 
-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_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}"