diff -r 40f815edbde4 -r 93938cafc0e6 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Jun 05 21:55:08 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Jun 05 15:59:20 2009 -0700
@@ -1170,8 +1170,6 @@
 
 subsection{* Limits, defined as vacuously true when the limit is trivial. *}
 
-notation tendsto (infixr "--->" 55)
-
   text{* Notation Lim to avoid collition with lim defined in analysis *}
 definition "Lim net f = (THE l. (f ---> l) net)"