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/Nonstandard_Analysis/HSeries.thy
changeset 80914 d97fdabd9e2b
parent 75866 9eeed5c424f9 
--- a/src/HOL/Nonstandard_Analysis/HSeries.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Nonstandard_Analysis/HSeries.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -14,7 +14,7 @@
 definition sumhr :: "hypnat \<times> hypnat \<times> (nat \<Rightarrow> real) \<Rightarrow> hypreal"
   where "sumhr = (\<lambda>(M,N,f). starfun2 (\<lambda>m n. sum f {m..<n}) M N)"
 
-definition NSsums :: "(nat \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"  (infixr "NSsums" 80)
+definition NSsums :: "(nat \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"  (infixr \<open>NSsums\<close> 80)
   where "f NSsums s = (\<lambda>n. sum f {..<n}) \<longlonglongrightarrow>\<^sub>N\<^sub>S s"
 
 definition NSsummable :: "(nat \<Rightarrow> real) \<Rightarrow> bool"
isabelle