Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/Gamma_Function.thy
changeset 80521 5c691b178e08
parent 79857 819c28a7280f 
--- a/src/HOL/Analysis/Gamma_Function.thy	Fri Jul 05 21:59:43 2024 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Sat Jul 06 12:51:31 2024 +0100
@@ -2756,7 +2756,7 @@
           exp (z * of_real (\<Sum>k = 1..n. ln (1 + 1 / real_of_nat k)))"
     by (subst exp_sum [symmetric]) (simp_all add: sum_distrib_left)
   also have "(\<Sum>k=1..n. ln (1 + 1 / of_nat k) :: real) = ln (\<Prod>k=1..n. 1 + 1 / real_of_nat k)"
-    by (subst ln_prod [symmetric]) (auto intro!: add_pos_nonneg)
+    by (subst ln_prod [symmetric]) (auto simp: divide_simps)
   also have "(\<Prod>k=1..n. 1 + 1 / of_nat k :: real) = (\<Prod>k=1..n. (of_nat k + 1) / of_nat k)"
     by (intro prod.cong) (simp_all add: field_split_simps)
   also have "(\<Prod>k=1..n. (of_nat k + 1) / of_nat k :: real) = of_nat n + 1"
isabelle