diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -1812,13 +1812,13 @@
   shows   "G x = Gamma x"
 proof (rule antisym)
   show "G x \<ge> Gamma x"
-  proof (rule tendsto_ge_const)
+  proof (rule tendsto_upperbound)
     from G_lower[of x] show "eventually (\<lambda>n. Gamma_series x n \<le> G x) sequentially"
       using eventually_ge_at_top[of "1::nat"] x by (auto elim!: eventually_mono)
   qed (simp_all add: Gamma_series_LIMSEQ)
 next
   show "G x \<le> Gamma x"
-  proof (rule tendsto_le_const)
+  proof (rule tendsto_lowerbound)
     have "(\<lambda>n. Gamma_series x n * (1 + x / real n)) \<longlonglongrightarrow> Gamma x * (1 + 0)"
       by (rule tendsto_intros real_tendsto_divide_at_top 
                Gamma_series_LIMSEQ filterlim_real_sequentially)+