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/HSEQ.thy
changeset 81142 6ad2c917dd2e
parent 80914 d97fdabd9e2b 
--- a/src/HOL/Nonstandard_Analysis/HSEQ.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -16,7 +16,7 @@
 begin
 
 definition NSLIMSEQ :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
-    (\<open>((_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))\<close> [60, 60] 60) where
+    (\<open>(\<open>notation=\<open>mixfix NSLIMSEQ\<close>\<close>(_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))\<close> [60, 60] 60) where
     \<comment> \<open>Nonstandard definition of convergence of sequence\<close>
   "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
isabelle