doc-src/TutorialI/Documents/document/Documents.tex

--- a/doc-src/TutorialI/Documents/document/Documents.tex	Sat Apr 28 11:24:20 2012 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Sat Apr 28 16:06:30 2012 +0200
@@ -182,10 +182,10 @@
 \endisadelimML
 %
 \begin{isamarkuptext}%
-\noindent The X-Symbol package within Proof~General provides several
-  input methods to enter \isa{{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}} in the text.  If all fails one may
-  just type a named entity \verb,\,\verb,<oplus>, by hand; the
-  corresponding symbol will be displayed after further input.
+\noindent Proof~General provides several input methods to enter
+  \isa{{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}} in the text.  If all fails one may just type a named
+  entity \verb,\,\verb,<oplus>, by hand; the corresponding symbol will
+  be displayed after further input.
 
   More flexible is to provide alternative syntax forms
   through the \bfindex{print mode} concept~\cite{isabelle-ref}.  By