1.1 --- a/src/HOL/Lim.thy	Fri Aug 19 10:46:54 2011 -0700
     1.2 +++ b/src/HOL/Lim.thy	Fri Aug 19 11:49:53 2011 -0700
     1.3 @@ -419,9 +419,13 @@
     1.4    shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a"
     1.5    unfolding isCont_def by (rule tendsto_divide)
     1.6  
     1.7 +lemma isCont_tendsto_compose:
     1.8 +  "\<lbrakk>isCont g l; (f ---> l) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
     1.9 +  unfolding isCont_def by (rule tendsto_compose)
    1.10 +
    1.11  lemma isCont_LIM_compose:
    1.12    "\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
    1.13 -  unfolding isCont_def by (rule LIM_compose)
    1.14 +  by (rule isCont_tendsto_compose) (* TODO: delete? *)
    1.15  
    1.16  lemma metric_isCont_LIM_compose2:
    1.17    assumes f [unfolded isCont_def]: "isCont f a"