--- a/src/HOL/Hyperreal/Lim.thy Wed Sep 20 07:42:12 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Wed Sep 20 07:44:34 2006 +0200
@@ -74,7 +74,7 @@
-section{*Some Purely Standard Proofs*}
+subsection{*Some Purely Standard Proofs*}
lemma LIM_eq:
"f -- a --> L =