diff -r f4bb3068d819 -r 22b87ab47d3b src/Doc/Tutorial/Documents/Documents.thy
--- a/src/Doc/Tutorial/Documents/Documents.thy	Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy	Fri Oct 31 11:18:17 2014 +0100
@@ -102,9 +102,8 @@
   Here $ident$ is any sequence of letters. 
   This results in an infinite store of symbols, whose
   interpretation is left to further front-end tools.  For example, the
-  user-interface of Proof~General + X-Symbol and the Isabelle document
-  processor (see \S\ref{sec:document-preparation}) display the
-  \verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
+  Isabelle document processor (see \S\ref{sec:document-preparation})
+  display the \verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
 
   A list of standard Isabelle symbols is given in
   @{cite "isabelle-isar-ref"}.  You may introduce your own
@@ -147,12 +146,7 @@
 (*>*)
 
 text {*
-  \noindent Proof~General provides several input methods to enter
-  @{text \<oplus>} 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
+  It is possible to provide alternative syntax forms
   through the \bfindex{print mode} concept~@{cite "isabelle-isar-ref"}.  By
   convention, the mode of ``$xsymbols$'' is enabled whenever
   Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now