src/HOL/Transcendental.thy

--- a/src/HOL/Transcendental.thy	Tue Aug 22 14:34:26 2017 +0200
+++ b/src/HOL/Transcendental.thy	Tue Aug 22 21:36:48 2017 +0200
@@ -1313,6 +1313,9 @@
   for A :: "'a::real_normed_field set"
   by (intro continuous_at_imp_continuous_on ballI isCont_pochhammer)
 
+lemmas continuous_on_pochhammer' [continuous_intros] =
+  continuous_on_compose2[OF continuous_on_pochhammer _ subset_UNIV]
+
 
 subsection \<open>Exponential Function\<close>