src/HOL/Nonstandard_Analysis/HSEQ.thy

--- a/src/HOL/Nonstandard_Analysis/HSEQ.thy	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy	Tue Aug 02 17:35:18 2016 +0200
@@ -11,7 +11,8 @@
 section \<open>Sequences and Convergence (Nonstandard)\<close>
 
 theory HSEQ
-imports Limits NatStar
+  imports Limits NatStar
+  abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
 begin
 
 definition