# HG changeset patch
# User wenzelm
# Date 1445542468 -7200
# Node ID a7ae3ef886a9a635879e9269eae78dd8b8451c41
# Parent  28e788ca2c5df2db983ece00617f1aa41d12583c
tuned;

diff -r 28e788ca2c5d -r a7ae3ef886a9 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Thu Oct 22 21:16:49 2015 +0200
+++ b/src/Doc/Implementation/ML.thy	Thu Oct 22 21:34:28 2015 +0200
@@ -1213,35 +1213,32 @@
 
 section \<open>Strings of symbols \label{sec:symbols}\<close>
 
-text \<open>A \<^emph>\<open>symbol\<close> constitutes the smallest textual unit in
-  Isabelle/ML --- raw ML characters are normally not encountered at
-  all.  Isabelle strings consist of a sequence of symbols, represented
-  as a packed string or an exploded list of strings.  Each symbol is
-  in itself a small string, which has either one of the following
-  forms:
-
-  \<^enum> a single ASCII character ``\<open>c\<close>'', for example ``\<^verbatim>\<open>a\<close>'',
-
-  \<^enum> a codepoint according to UTF-8 (non-ASCII byte sequence),
-
-  \<^enum> a regular symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>ident\<close>\<^verbatim>\<open>>\<close>'', for example ``\<^verbatim>\<open>\<alpha>\<close>'',
-
-  \<^enum> a control symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^\<close>\<open>ident\<close>\<^verbatim>\<open>>\<close>'', for example ``\<^verbatim>\<open>\<^bold>\<close>'',
-
-  \<^enum> a raw symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw:\<close>\<open>text\<close>\<^verbatim>\<open>>\<close>'' where \<open>text\<close> consists of printable characters
-  excluding ``\<^verbatim>\<open>.\<close>'' and ``\<^verbatim>\<open>>\<close>'', for example
-  ``\<^verbatim>\<open>\<^raw:$\sum_{i = 1}^n$>\<close>'',
-
-  \<^enum> a numbered raw control symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw\<close>\<open>n\<close>\<^verbatim>\<open>>\<close>, where \<open>n\<close> consists
-  of digits, for example ``\<^verbatim>\<open>\<^raw42>\<close>''.
-
-
-  The \<open>ident\<close> syntax for symbol names is \<open>letter
-  (letter | digit)\<^sup>*\<close>, where \<open>letter = A..Za..z\<close> and \<open>digit = 0..9\<close>.  There are infinitely many regular symbols and
-  control symbols, but a fixed collection of standard symbols is
-  treated specifically.  For example, ``\<^verbatim>\<open>\<alpha>\<close>'' is
-  classified as a letter, which means it may occur within regular
-  Isabelle identifiers.
+text \<open>A \<^emph>\<open>symbol\<close> constitutes the smallest textual unit in Isabelle/ML --- raw
+  ML characters are normally not encountered at all. Isabelle strings consist
+  of a sequence of symbols, represented as a packed string or an exploded list
+  of strings. Each symbol is in itself a small string, which has either one of
+  the following forms:
+
+    \<^enum> a single ASCII character ``\<open>c\<close>'', for example ``\<^verbatim>\<open>a\<close>'',
+
+    \<^enum> a codepoint according to UTF-8 (non-ASCII byte sequence),
+
+    \<^enum> a regular symbol ``\<^verbatim>\<open>\<ident>\<close>'', for example ``\<^verbatim>\<open>\<alpha>\<close>'',
+
+    \<^enum> a control symbol ``\<^verbatim>\<open>\<^ident>\<close>'', for example ``\<^verbatim>\<open>\<^bold>\<close>'',
+
+    \<^enum> a raw symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw:\<close>\<open>text\<close>\<^verbatim>\<open>>\<close>'' where \<open>text\<close> consists of
+    printable characters excluding ``\<^verbatim>\<open>.\<close>'' and ``\<^verbatim>\<open>>\<close>'', for example
+    ``\<^verbatim>\<open>\<^raw:$\sum_{i = 1}^n$>\<close>'',
+
+    \<^enum> a numbered raw control symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw\<close>\<open>n\<close>\<^verbatim>\<open>>\<close>, where \<open>n\<close> consists
+    of digits, for example ``\<^verbatim>\<open>\<^raw42>\<close>''.
+
+  The \<open>ident\<close> syntax for symbol names is \<open>letter (letter | digit)\<^sup>*\<close>, where
+  \<open>letter = A..Za..z\<close> and \<open>digit = 0..9\<close>. There are infinitely many regular
+  symbols and control symbols, but a fixed collection of standard symbols is
+  treated specifically. For example, ``\<^verbatim>\<open>\<alpha>\<close>'' is classified as a letter, which
+  means it may occur within regular Isabelle identifiers.
 
   The character set underlying Isabelle symbols is 7-bit ASCII, but 8-bit
   character sequences are passed-through unchanged. Unicode/UCS data in UTF-8
@@ -1251,11 +1248,11 @@
   to the standard collection of Isabelle regular symbols.
 
   \<^medskip>
-  Output of Isabelle symbols depends on the print mode. For example,
-  the standard {\LaTeX} setup of the Isabelle document preparation system
-  would present ``\<^verbatim>\<open>\<alpha>\<close>'' as \<open>\<alpha>\<close>, and ``\<^verbatim>\<open>\<^bold>\<alpha>\<close>'' as \<open>\<^bold>\<alpha>\<close>. On-screen rendering
-  usually works by mapping a finite subset of Isabelle symbols to suitable
-  Unicode characters.
+  Output of Isabelle symbols depends on the print mode. For example, the
+  standard {\LaTeX} setup of the Isabelle document preparation system would
+  present ``\<^verbatim>\<open>\<alpha>\<close>'' as \<open>\<alpha>\<close>, and ``\<^verbatim>\<open>\<^bold>\<alpha>\<close>'' as \<open>\<^bold>\<alpha>\<close>. On-screen rendering usually
+  works by mapping a finite subset of Isabelle symbols to suitable Unicode
+  characters.
 \<close>
 
 text %mlref \<open>
diff -r 28e788ca2c5d -r a7ae3ef886a9 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Oct 22 21:16:49 2015 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Oct 22 21:34:28 2015 +0200
@@ -135,7 +135,7 @@
   argument that is a cartouche.
 
   Omitting the control symbol is also possible: a cartouche without special
-  decoration is equivalent to \<^verbatim>\<open>\\<close>\<^verbatim>\<open><^cartouche>\<close>\<open>\<open>argument_content\<close>\<close>, which
+  decoration is equivalent to \<^verbatim>\<open>\<^cartouche>\<close>\<open>\<open>argument_content\<close>\<close>, which
   is equivalent to \<^verbatim>\<open>@{cartouche\<close>~\<open>\<open>argument_content\<close>\<close>\<^verbatim>\<open>}\<close>. The
   special name @{antiquotation_def cartouche} is defined in the context:
   Isabelle/Pure introduces that as an alias to @{antiquotation_ref text}
diff -r 28e788ca2c5d -r a7ae3ef886a9 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Thu Oct 22 21:16:49 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Thu Oct 22 21:34:28 2015 +0200
@@ -505,30 +505,26 @@
   This is a summary for practically relevant input methods for Isabelle
   symbols.
 
-  \<^enum> The \<^emph>\<open>Symbols\<close> panel: some GUI buttons allow to insert
-  certain symbols in the text buffer.  There are also tooltips to
-  reveal the official Isabelle representation with some additional
-  information about \<^emph>\<open>symbol abbreviations\<close> (see below).
+  \<^enum> The \<^emph>\<open>Symbols\<close> panel: some GUI buttons allow to insert certain symbols in
+  the text buffer. There are also tooltips to reveal the official Isabelle
+  representation with some additional information about \<^emph>\<open>symbol
+  abbreviations\<close> (see below).
 
-  \<^enum> Copy/paste from decoded source files: text that is rendered
-  as Unicode already can be re-used to produce further text.  This
-  also works between different applications, e.g.\ Isabelle/jEdit and
-  some web browser or mail client, as long as the same Unicode view on
-  Isabelle symbols is used.
+  \<^enum> Copy/paste from decoded source files: text that is rendered as Unicode
+  already can be re-used to produce further text. This also works between
+  different applications, e.g.\ Isabelle/jEdit and some web browser or mail
+  client, as long as the same Unicode view on Isabelle symbols is used.
 
-  \<^enum> Copy/paste from prover output within Isabelle/jEdit. The same
-  principles as for text buffers apply, but note that \<^emph>\<open>copy\<close> in secondary
-  Isabelle/jEdit windows works via the keyboard shortcuts \<^verbatim>\<open>C+c\<close> or
-  \<^verbatim>\<open>C+INSERT\<close>, while jEdit menu actions always refer to the primary
-  text area!
+  \<^enum> Copy/paste from prover output within Isabelle/jEdit. The same principles
+  as for text buffers apply, but note that \<^emph>\<open>copy\<close> in secondary Isabelle/jEdit
+  windows works via the keyboard shortcuts \<^verbatim>\<open>C+c\<close> or \<^verbatim>\<open>C+INSERT\<close>, while jEdit
+  menu actions always refer to the primary text area!
 
-  \<^enum> Completion provided by Isabelle plugin (see
-  \secref{sec:completion}).  Isabelle symbols have a canonical name
-  and optional abbreviations.  This can be used with the text
-  completion mechanism of Isabelle/jEdit, to replace a prefix of the
-  actual symbol like \<^verbatim>\<open>\<lambda>\<close>, or its name preceded by backslash
-  \<^verbatim>\<open>\\<close>\<^verbatim>\<open>lambda\<close>, or its ASCII abbreviation
-  \<^verbatim>\<open>%\<close> by the Unicode rendering.
+  \<^enum> Completion provided by Isabelle plugin (see \secref{sec:completion}).
+  Isabelle symbols have a canonical name and optional abbreviations. This can
+  be used with the text completion mechanism of Isabelle/jEdit, to replace a
+  prefix of the actual symbol like \<^verbatim>\<open>\<lambda>\<close>, or its name preceded by backslash
+  \<^verbatim>\<open>\lambda\<close>, or its ASCII abbreviation \<^verbatim>\<open>%\<close> by the Unicode rendering.
 
   The following table is an extract of the information provided by the
   standard @{file "$ISABELLE_HOME/etc/symbols"} file:
@@ -565,13 +561,12 @@
   \secref{sec:completion}).
 
 
-  \paragraph{Control symbols.} There are some special control symbols
-  to modify the display style of a single symbol (without
-  nesting). Control symbols may be applied to a region of selected
-  text, either using the \<^emph>\<open>Symbols\<close> panel or keyboard shortcuts or
-  jEdit actions.  These editor operations produce a separate control
-  symbol for each symbol in the text, in order to make the whole text
-  appear in a certain style.
+  \paragraph{Control symbols.} There are some special control symbols to
+  modify the display style of a single symbol (without nesting). Control
+  symbols may be applied to a region of selected text, either using the
+  \<^emph>\<open>Symbols\<close> panel or keyboard shortcuts or jEdit actions. These editor
+  operations produce a separate control symbol for each symbol in the text, in
+  order to make the whole text appear in a certain style.
 
   \<^medskip>
   \begin{tabular}{llll}
@@ -585,8 +580,7 @@
   \<^medskip>
 
   To produce a single control symbol, it is also possible to complete on
-  \<^verbatim>\<open>\\<close>\<^verbatim>\<open>sup\<close>, \<^verbatim>\<open>\\<close>\<^verbatim>\<open>sub\<close>, \<^verbatim>\<open>\\<close>\<^verbatim>\<open>bold\<close>, \<^verbatim>\<open>\\<close>\<^verbatim>\<open>emph\<close> as for regular
-  symbols.
+  \<^verbatim>\<open>\sup\<close>, \<^verbatim>\<open>\sub\<close>, \<^verbatim>\<open>\bold\<close>, \<^verbatim>\<open>\emph\<close> as for regular symbols.
 
   The emphasized style only takes effect in document output, not in the
   editor.
diff -r 28e788ca2c5d -r a7ae3ef886a9 src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Thu Oct 22 21:16:49 2015 +0200
+++ b/src/Doc/System/Presentation.thy	Thu Oct 22 21:34:28 2015 +0200
@@ -233,7 +233,7 @@
   includes an appropriate path specification for {\TeX} inputs.
 
   If the text contains any references to Isabelle symbols (such as
-  \<^verbatim>\<open>\\<close>\<^verbatim>\<open><forall>\<close>) then \<^verbatim>\<open>isabellesym.sty\<close> should be included as well.
+  \<^verbatim>\<open>\<forall>\<close>) then \<^verbatim>\<open>isabellesym.sty\<close> should be included as well.
   This package contains a standard set of {\LaTeX} macro definitions
   \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>,
   see @{cite "isabelle-implementation"} for a