# HG changeset patch
# User huffman
# Date 1313779793 25200
# Node ID ba3d031b5dbbaba1f04d042bd84fd6ccf82ba974
# Parent  d2a6f9af02f467aecd9dce5f71b7f63278d92765
add lemma isCont_tendsto_compose

diff -r d2a6f9af02f4 -r ba3d031b5dbb src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/HOL/Lim.thy	Fri Aug 19 11:49:53 2011 -0700
@@ -419,9 +419,13 @@
   shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a"
   unfolding isCont_def by (rule tendsto_divide)
 
+lemma isCont_tendsto_compose:
+  "\<lbrakk>isCont g l; (f ---> l) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
+  unfolding isCont_def by (rule tendsto_compose)
+
 lemma isCont_LIM_compose:
   "\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
-  unfolding isCont_def by (rule LIM_compose)
+  by (rule isCont_tendsto_compose) (* TODO: delete? *)
 
 lemma metric_isCont_LIM_compose2:
   assumes f [unfolded isCont_def]: "isCont f a"