# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1710245488 0
# Node ID fed0a3c60e2b819126aeda1eeac626b56af9c126
# Parent  819c28a7280f9fff2e1fb0ee5019f7e80e7f8843
Fixed a latex error in the markup

diff -r 819c28a7280f -r fed0a3c60e2b src/HOL/Complex_Analysis/Meromorphic.thy
--- a/src/HOL/Complex_Analysis/Meromorphic.thy	Mon Mar 11 15:07:02 2024 +0000
+++ b/src/HOL/Complex_Analysis/Meromorphic.thy	Tue Mar 12 12:11:28 2024 +0000
@@ -59,7 +59,7 @@
   shows   "(\<lambda>y. \<Prod>x\<in>#I. f x y) has_laurent_expansion (\<Prod>x\<in>#I. F x)"
   using assms by (induction I) (auto intro!: laurent_expansion_intros)
 
-subsection \<open>Remove singular points: remove_sings\<close>
+subsection \<open>Remove singular points\<close>
 
 definition remove_sings :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex" where
   "remove_sings f z = (if \<exists>c. f \<midarrow>z\<rightarrow> c then Lim (at z) f else 0)"