diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Nonstandard_Analysis/HSEQ.thy
--- 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)"