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/Series.thy
changeset 80932 261cd8722677
parent 77491 9d431c939a7f 
--- a/src/HOL/Series.thy	Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Series.thy	Mon Sep 23 13:32:38 2024 +0200
@@ -16,14 +16,14 @@
 subsection \<open>Definition of infinite summability\<close>
 
 definition sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool"
-    (infixr "sums" 80)
+    (infixr \<open>sums\<close> 80)
   where "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> s"
 
 definition summable :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> bool"
   where "summable f \<longleftrightarrow> (\<exists>s. f sums s)"
 
 definition suminf :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a"
-    (binder "\<Sum>" 10)
+    (binder \<open>\<Sum>\<close> 10)
   where "suminf f = (THE s. f sums s)"
 
 text\<open>Variants of the definition\<close>
isabelle