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/Complex_Analysis/Laurent_Convergence.thy
changeset 80914 d97fdabd9e2b
parent 79945 ca004ccf2352
child 80948 572970d15ab0 
--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -102,7 +102,7 @@
 
 definition\<^marker>\<open>tag important\<close>
   has_laurent_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex fls \<Rightarrow> bool"
-  (infixl "has'_laurent'_expansion" 60)
+  (infixl \<open>has'_laurent'_expansion\<close> 60)
   where "(f has_laurent_expansion F) \<longleftrightarrow>
             fls_conv_radius F > 0 \<and> eventually (\<lambda>z. eval_fls F z = f z) (at 0)"
isabelle