diff -r 179ff9cb160b -r 5b25fee0362c doc-src/IsarRef/Thy/document/Outer_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Wed Mar 04 10:43:39 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Wed Mar 04 10:45:52 2009 +0100
@@ -3,8 +3,6 @@
 \def\isabellecontext{Outer{\isacharunderscore}Syntax}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
@@ -185,10 +183,10 @@
   Isabelle as \verb|\<forall>|.  There are infinitely many Isabelle
   symbols like this, although proper presentation is left to front-end
   tools such as {\LaTeX} or Proof~General with the X-Symbol package.
-  A list of standard Isabelle symbols that work well with these tools
-  is given in \appref{app:symbols}.  Note that \verb|\<lambda>| does
-  not belong to the \isa{letter} category, since it is already used
-  differently in the Pure term language.%
+  A list of predefined Isabelle symbols that work well with these
+  tools is given in \appref{app:symbols}.  Note that \verb|\<lambda>|
+  does not belong to the \isa{letter} category, since it is already
+  used differently in the Pure term language.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %