--- 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%
%