# HG changeset patch
# User wenzelm
# Date 1601300232 -7200
# Node ID bc97bd4c0474415e2374a55b5f84e23a781574e9
# Parent  d24a8cea343bbc422f348cb419b4c44c66e722ab
prefer old-fashioned {\ss} to prevent problems with encoding in lualatex;

diff -r d24a8cea343b -r bc97bd4c0474 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Mon Sep 28 14:55:37 2020 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Mon Sep 28 15:37:12 2020 +0200
@@ -18,7 +18,7 @@
   most important properties. Also contains the definition and some properties
   of the log-Gamma function and the Digamma function and the other Polygamma functions.
 
-  Based on the Gamma function, we also prove the Weierstraß product form of the
+  Based on the Gamma function, we also prove the Weierstra{\ss} product form of the
   sin function and, based on this, the solution of the Basel problem (the
   sum over all \<^term>\<open>1 / (n::nat)^2\<close>.
 \<close>
@@ -3349,7 +3349,7 @@
 qed
 
 
-subsection \<open>The Weierstraß product formula for the sine\<close>
+subsection \<open>The Weierstra{\ss} product formula for the sine\<close>
 
 theorem sin_product_formula_complex:
   fixes z :: complex