# HG changeset patch
# User wenzelm
# Date 1413833574 -7200
# Node ID e5f809f52f26df15d99bc02a534682cd077320f0
# Parent  33be43d701474b386ba82140c0674a9799148da6
more antiquotations;
tuned spacing;

diff -r 33be43d70147 -r e5f809f52f26 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Oct 20 20:43:02 2014 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Oct 20 21:32:54 2014 +0200
@@ -59,25 +59,22 @@
 
   \item @{command header} provides plain text markup just preceding
   the formal beginning of a theory.  The corresponding {\LaTeX} macro
-  is @{verbatim "\\isamarkupheader"}, which acts like @{command
+  is @{verbatim \<open>\isamarkupheader\<close>}, which acts like @{command
   section} by default.
   
   \item @{command chapter}, @{command section}, @{command subsection},
   and @{command subsubsection} mark chapter and section headings
   within the main theory body or local theory targets.  The
-  corresponding {\LaTeX} macros are @{verbatim "\\isamarkupchapter"},
-  @{verbatim "\\isamarkupsection"}, @{verbatim
-  "\\isamarkupsubsection"} etc.
+  corresponding {\LaTeX} macros are @{verbatim \<open>\isamarkupchapter\<close>},
+  @{verbatim \<open>\isamarkupsection\<close>}, @{verbatim \<open>\isamarkupsubsection\<close>} etc.
 
   \item @{command sect}, @{command subsect}, and @{command subsubsect}
   mark section headings within proofs.  The corresponding {\LaTeX}
-  macros are @{verbatim "\\isamarkupsect"}, @{verbatim
-  "\\isamarkupsubsect"} etc.
+  macros are @{verbatim \<open>\isamarkupsect\<close>}, @{verbatim \<open>\isamarkupsubsect\<close>} etc.
 
   \item @{command text} and @{command txt} specify paragraphs of plain
   text.  This corresponds to a {\LaTeX} environment @{verbatim
-  "\\begin{isamarkuptext}"} @{text "\<dots>"} @{verbatim
-  "\\end{isamarkuptext}"} etc.
+  \<open>\begin{isamarkuptext}\<close>} @{text "\<dots>"} @{verbatim \<open>\end{isamarkuptext}\<close>} etc.
 
   \item @{command text_raw} and @{command txt_raw} insert {\LaTeX}
   source into the output, without additional markup.  Thus the full
@@ -139,7 +136,7 @@
   in the resulting document, but may again refer to formal entities
   via \emph{document antiquotations}.
 
-  For example, embedding of ``@{text [source=false] "@{term [show_types] \"f x = a + x\"}"}''
+  For example, embedding @{verbatim \<open>@{term [show_types] "f x = a + x"}\<close>}
   within a text block makes
   \isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} appear in the final {\LaTeX} document.
 
@@ -287,18 +284,18 @@
   results in an active hyperlink within the text.
 
   \item @{text "@{cite name}"} produces a citation @{verbatim
-  "\\cite{name}"} in {\LaTeX}, where the name refers to some Bib{\TeX}
+  \<open>\cite{name}\<close>} in {\LaTeX}, where the name refers to some Bib{\TeX}
   database entry.
 
   The variant @{text "@{cite \<open>opt\<close> name}"} produces @{verbatim
-  "\\cite[opt]{name}"} with some free-form optional argument. Multiple names
+  \<open>\cite[opt]{name}\<close>} with some free-form optional argument. Multiple names
   are output with commas, e.g. @{text "@{cite foo \<AND> bar}"} becomes
-  @{verbatim "\\cite{foo,bar}"}.
+  @{verbatim \<open>\cite{foo,bar}\<close>}.
 
   The {\LaTeX} macro name is determined by the antiquotation option
   @{antiquotation_option_def cite_macro}, or the configuration option
   @{attribute cite_macro} in the context. For example, @{text "@{cite
-  [cite_macro = nocite] foobar}"} produces @{verbatim "\\nocite{foobar}"}.
+  [cite_macro = nocite] foobar}"} produces @{verbatim \<open>\nocite{foobar}\<close>}.
 
   \end{description}
 \<close>
@@ -487,7 +484,7 @@
   The @{antiquotation rail} antiquotation allows to include syntax
   diagrams into Isabelle documents.  {\LaTeX} requires the style file
   @{file "~~/lib/texinputs/pdfsetup.sty"}, which can be used via
-  @{verbatim "\\usepackage{pdfsetup}"} in @{verbatim "root.tex"}, for
+  @{verbatim \<open>\usepackage{pdfsetup}\<close>} in @{verbatim "root.tex"}, for
   example.
 
   The rail specification language is quoted here as Isabelle @{syntax
diff -r 33be43d70147 -r e5f809f52f26 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Oct 20 20:43:02 2014 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Oct 20 21:32:54 2014 +0200
@@ -288,7 +288,7 @@
 
   \begin{itemize}
 
-  \item @{verbatim "\"\""} (the empty string): default mode;
+  \item @{verbatim \<open>""\<close>} (the empty string): default mode;
   implicitly active as last element in the list of modes.
 
   \item @{verbatim input}: dummy print mode that is never active; may
@@ -447,20 +447,20 @@
   \begin{center}
   \begin{tabular}{lll}
 
-  @{verbatim "("}@{keyword_def "infix"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
+  @{verbatim "("}@{keyword_def "infix"}~@{verbatim \<open>"\<close>}@{text sy}@{verbatim \<open>"\<close>} @{text "p"}@{verbatim ")"}
   & @{text "\<mapsto>"} &
-  @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p + 1"}@{verbatim ", "}@{text "p + 1"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
-  @{verbatim "("}@{keyword_def "infixl"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
+  @{verbatim \<open>("(_\<close>}~@{text sy}@{verbatim \<open>/ _)" [\<close>}@{text "p + 1"}@{verbatim ","}~@{text "p + 1"}@{verbatim "]"}~@{text "p"}@{verbatim ")"} \\
+  @{verbatim "("}@{keyword_def "infixl"}~@{verbatim \<open>"\<close>}@{text sy}@{verbatim \<open>"\<close>} @{text "p"}@{verbatim ")"}
   & @{text "\<mapsto>"} &
-  @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p"}@{verbatim ", "}@{text "p + 1"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
-  @{verbatim "("}@{keyword_def "infixr"}~@{verbatim "\""}@{text sy}@{verbatim "\""} @{text "p"}@{verbatim ")"}
+  @{verbatim \<open>("(_\<close>}~@{text sy}@{verbatim \<open>/ _)" [\<close>}@{text "p"}@{verbatim ","}~@{text "p + 1"}@{verbatim "]"}~@{text "p"}@{verbatim ")"} \\
+  @{verbatim "("}@{keyword_def "infixr"}~@{verbatim \<open>"\<close>}@{text sy}@{verbatim \<open>"\<close>}~@{text "p"}@{verbatim ")"}
   & @{text "\<mapsto>"} &
-  @{verbatim "(\"(_ "}@{text sy}@{verbatim "/ _)\" ["}@{text "p + 1"}@{verbatim ", "}@{text "p"}@{verbatim "]"}@{text " p"}@{verbatim ")"} \\
+  @{verbatim \<open>("(_\<close>}~@{text sy}@{verbatim \<open>/ _)" [\<close>}@{text "p + 1"}@{verbatim ","}~@{text "p"}@{verbatim "]"}~@{text "p"}@{verbatim ")"} \\
 
   \end{tabular}
   \end{center}
 
-  The mixfix template @{verbatim "\"(_ "}@{text sy}@{verbatim "/ _)\""}
+  The mixfix template @{verbatim \<open>"(_\<close>}~@{text sy}@{verbatim \<open>/ _)"\<close>}
   specifies two argument positions; the delimiter is preceded by a
   space and followed by a space or line break; the entire phrase is a
   pretty printing block.
@@ -481,7 +481,7 @@
   as follows:
 
   \begin{center}
-  @{text "c :: "}@{verbatim "\""}@{text "(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3"}@{verbatim "\"  ("}@{keyword "binder"}@{verbatim " \""}@{text "sy"}@{verbatim "\" ["}@{text "p"}@{verbatim "] "}@{text "q"}@{verbatim ")"}
+  @{text "c :: "}@{verbatim \<open>"\<close>}@{text "(\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2) \<Rightarrow> \<tau>\<^sub>3"}@{verbatim \<open>"  (\<close>}@{keyword "binder"}~@{verbatim \<open>"\<close>}@{text "sy"}@{verbatim \<open>" [\<close>}@{text "p"}@{verbatim "]"}~@{text "q"}@{verbatim ")"}
   \end{center}
 
   This introduces concrete binder syntax @{text "sy x. b"}, where
@@ -493,13 +493,13 @@
 
   Internally, the binder syntax is expanded to something like this:
   \begin{center}
-  @{text "c_binder :: "}@{verbatim "\""}@{text "idts \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3"}@{verbatim "\"  (\"(3"}@{text sy}@{verbatim "_./ _)\" [0, "}@{text "p"}@{verbatim "] "}@{text "q"}@{verbatim ")"}
+  @{text "c_binder :: "}@{verbatim \<open>"\<close>}@{text "idts \<Rightarrow> \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3"}@{verbatim \<open>"  ("(3\<close>}@{text sy}@{verbatim \<open>_./ _)" [0,\<close>}~@{text "p"}@{verbatim "]"}~@{text "q"}@{verbatim ")"}
   \end{center}
 
   Here @{syntax (inner) idts} is the nonterminal symbol for a list of
   identifiers with optional type constraints (see also
   \secref{sec:pure-grammar}).  The mixfix template @{verbatim
-  "\"(3"}@{text sy}@{verbatim "_./ _)\""} defines argument positions
+  \<open>"(3\<close>}@{text sy}@{verbatim \<open>_./ _)"\<close>} defines argument positions
   for the bound identifiers and the body, separated by a dot with
   optional line break; the entire phrase is a pretty printing block of
   indentation level 3.  Note that there is no extra space after @{text
@@ -602,7 +602,7 @@
     @{syntax_def (inner) num_token} & = & @{syntax_ref nat} \\
     @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
     @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
-    @{syntax_def (inner) string_token} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
+    @{syntax_def (inner) string_token} & = & @{verbatim \<open>"\<close>} @{text "\<dots>"} @{verbatim \<open>"\<close>} \\
     @{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
   \end{supertabular}
   \end{center}
@@ -1063,9 +1063,8 @@
   shown as quoted strings, variable atoms as non-quoted strings and
   applications as a parenthesized list of subtrees.  For example, the
   AST
-  @{ML [display] "Ast.Appl
-  [Ast.Constant \"_abs\", Ast.Variable \"x\", Ast.Variable \"t\"]"}
-  is pretty-printed as @{verbatim "(\"_abs\" x t)"}.  Note that
+  @{ML [display] \<open>Ast.Appl [Ast.Constant "_abs", Ast.Variable "x", Ast.Variable "t"]\<close>}
+  is pretty-printed as @{verbatim \<open>("_abs" x t)\<close>}.  Note that
   @{verbatim "()"} and @{verbatim "(x)"} are excluded as ASTs, because
   they have too few subtrees.
 
@@ -1074,11 +1073,11 @@
   either term application or type application, depending on the
   syntactic context.
 
-  Nested application like @{verbatim "((\"_abs\" x t) u)"} is also
+  Nested application like @{verbatim \<open>(("_abs" x t) u)\<close>} is also
   possible, but ASTs are definitely first-order: the syntax constant
-  @{verbatim "\"_abs\""} does not bind the @{verbatim x} in any way.
+  @{verbatim \<open>"_abs"\<close>} does not bind the @{verbatim x} in any way.
   Proper bindings are introduced in later stages of the term syntax,
-  where @{verbatim "(\"_abs\" x t)"} becomes an @{ML Abs} node and
+  where @{verbatim \<open>("_abs" x t)\<close>} becomes an @{ML Abs} node and
   occurrences of @{verbatim x} in @{verbatim t} are replaced by bound
   variables (represented as de-Bruijn indices).
 \<close>
@@ -1209,7 +1208,7 @@
 
   \item @{command "syntax"}~@{text "(mode) c :: \<sigma> (mx)"} augments the
   priority grammar and the pretty printer table for the given print
-  mode (default @{verbatim "\"\""}). An optional keyword @{keyword_ref
+  mode (default @{verbatim \<open>""\<close>}). An optional keyword @{keyword_ref
   "output"} means that only the pretty printer table is affected.
 
   Following \secref{sec:mixfix}, the mixfix annotation @{text "mx =
@@ -1251,7 +1250,7 @@
   with other syntax declarations.
 
   \medskip The special case of copy production is specified by @{text
-  "c = "}@{verbatim "\"\""} (empty string).  It means that the
+  "c = "}@{verbatim \<open>""\<close>} (empty string).  It means that the
   resulting parse tree @{text "t"} is copied directly, without any
   further decoration.
 
@@ -1587,10 +1586,10 @@
   @{text "f x y z"} & @{verbatim "(f x y z)"} \\
   @{text "'a ty"} & @{verbatim "(ty 'a)"} \\
   @{text "('a, 'b)ty"} & @{verbatim "(ty 'a 'b)"} \\
-  @{text "\<lambda>x y z. t"} & @{verbatim "(\"_abs\" x (\"_abs\" y (\"_abs\" z t)))"} \\
-  @{text "\<lambda>x :: 'a. t"} & @{verbatim "(\"_abs\" (\"_constrain\" x 'a) t)"} \\
-  @{text "\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S"} & @{verbatim "(\"==>\" P (\"==>\" Q (\"==>\" R S)))"} \\
-   @{text "['a, 'b, 'c] \<Rightarrow> 'd"} & @{verbatim "(\"fun\" 'a (\"fun\" 'b (\"fun\" 'c 'd)))"} \\
+  @{text "\<lambda>x y z. t"} & @{verbatim \<open>("_abs" x ("_abs" y ("_abs" z t)))\<close>} \\
+  @{text "\<lambda>x :: 'a. t"} & @{verbatim \<open>("_abs" ("_constrain" x 'a) t)\<close>} \\
+  @{text "\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S"} & @{verbatim \<open>("==>" P ("==>" Q ("==>" R S)))\<close>} \\
+   @{text "['a, 'b, 'c] \<Rightarrow> 'd"} & @{verbatim \<open>("fun" 'a ("fun" 'b ("fun" 'c 'd)))\<close>} \\
   \end{tabular}
   \end{center}
 
@@ -1618,8 +1617,8 @@
 
   The outcome is still a first-order term.  Proper abstractions and
   bound variables are introduced by parse translations associated with
-  certain syntax constants.  Thus @{verbatim "(_abs x x)"} eventually
-  becomes a de-Bruijn term @{verbatim "Abs (\"x\", _, Bound 0)"}.
+  certain syntax constants.  Thus @{verbatim \<open>("_abs" x x)\<close>} eventually
+  becomes a de-Bruijn term @{verbatim \<open>Abs ("x", _, Bound 0)\<close>}.
 \<close>
 
 
diff -r 33be43d70147 -r e5f809f52f26 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon Oct 20 20:43:02 2014 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon Oct 20 21:32:54 2014 +0200
@@ -22,7 +22,7 @@
   syntax is that of Isabelle/Isar theory sources (specifications and
   proofs).  As a general rule, inner syntax entities may occur only as
   \emph{atomic entities} within outer syntax.  For example, the string
-  @{verbatim "\"x + y\""} and identifier @{verbatim z} are legal term
+  @{verbatim \<open>"x + y"\<close>} and identifier @{verbatim z} are legal term
   specifications within a theory, while @{verbatim "x + y"} without
   quotes is not.
 
@@ -123,7 +123,7 @@
 
   Keywords override named tokens.  For example, the presence of a
   command called @{verbatim term} inhibits the identifier @{verbatim
-  term}, but the string @{verbatim "\"term\""} can be used instead.
+  term}, but the string @{verbatim \<open>"term"\<close>} can be used instead.
   By convention, the outer syntax always allows quoted strings in
   addition to identifiers, wherever a named entity is expected.
 
@@ -139,18 +139,18 @@
   \begin{supertabular}{rcl}
     @{syntax_def ident} & = & @{text "letter (subscript\<^sup>? quasiletter)\<^sup>*"} \\
     @{syntax_def longident} & = & @{text "ident("}@{verbatim "."}@{text "ident)\<^sup>+"} \\
-    @{syntax_def symident} & = & @{text "sym\<^sup>+  |  "}@{verbatim "\\"}@{verbatim "<"}@{text ident}@{verbatim ">"} \\
+    @{syntax_def symident} & = & @{text "sym\<^sup>+  |  "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text ident}@{verbatim ">"} \\
     @{syntax_def nat} & = & @{text "digit\<^sup>+"} \\
     @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
     @{syntax_def var} & = & @{verbatim "?"}@{text "ident  |  "}@{verbatim "?"}@{text ident}@{verbatim "."}@{text nat} \\
     @{syntax_def typefree} & = & @{verbatim "'"}@{text ident} \\
     @{syntax_def typevar} & = & @{verbatim "?"}@{text "typefree  |  "}@{verbatim "?"}@{text typefree}@{verbatim "."}@{text nat} \\
-    @{syntax_def string} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
+    @{syntax_def string} & = & @{verbatim \<open>"\<close>} @{text "\<dots>"} @{verbatim \<open>"\<close>} \\
     @{syntax_def altstring} & = & @{verbatim "`"} @{text "\<dots>"} @{verbatim "`"} \\
     @{syntax_def cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
     @{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*"}@{verbatim "}"} \\[1ex]
 
-    @{text letter} & = & @{text "latin  |  "}@{verbatim "\\"}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text "  |  "}@{verbatim "\\"}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text "  |  greek  |"} \\
+    @{text letter} & = & @{text "latin  |  "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text "  |  "}@{verbatim \<open>\\<close>}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text "  |  greek  |"} \\
     @{text subscript} & = & @{verbatim "\<^sub>"} \\
     @{text quasiletter} & = & @{text "letter  |  digit  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "'"} \\
     @{text latin} & = & @{verbatim a}@{text "  | \<dots> |  "}@{verbatim z}@{text "  |  "}@{verbatim A}@{text "  |  \<dots> |  "}@{verbatim Z} \\
@@ -178,9 +178,9 @@
   same unknown, with basename @{text "x"} and index 0.
 
   The syntax of @{syntax_ref string} admits any characters, including
-  newlines; ``@{verbatim "\""}'' (double-quote) and ``@{verbatim
-  "\\"}'' (backslash) need to be escaped by a backslash; arbitrary
-  character codes may be specified as ``@{verbatim "\\"}@{text ddd}'',
+  newlines; ``@{verbatim \<open>"\<close>}'' (double-quote) and ``@{verbatim \<open>\\<close>}''
+  (backslash) need to be escaped by a backslash; arbitrary
+  character codes may be specified as ``@{verbatim \<open>\\<close>}@{text ddd}'',
   with three decimal digits.  Alternative strings according to
   @{syntax_ref altstring} are analogous, using single back-quotes
   instead.
@@ -229,7 +229,7 @@
   constants, theorems etc.\ that are to be \emph{declared} or
   \emph{defined} (so qualified identifiers are excluded here).  Quoted
   strings provide an escape for non-identifier names or those ruled
-  out by outer syntax keywords (e.g.\ quoted @{verbatim "\"let\""}).
+  out by outer syntax keywords (e.g.\ quoted @{verbatim \<open>"let"\<close>}).
   Already existing objects are usually referenced by @{syntax
   nameref}.
 
@@ -308,7 +308,7 @@
   is performed internally later).  For convenience, a slightly more
   liberal convention is adopted: quotes may be omitted for any type or
   term that is already atomic at the outer level.  For example, one
-  may just write @{verbatim x} instead of quoted @{verbatim "\"x\""}.
+  may just write @{verbatim x} instead of quoted @{verbatim \<open>"x"\<close>}.
   Note that symbolic identifiers (e.g.\ @{verbatim "++"} or @{text
   "\<forall>"} are available as well, provided these have not been superseded
   by commands or other keywords already (such as @{verbatim "="} or
diff -r 33be43d70147 -r e5f809f52f26 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Oct 20 20:43:02 2014 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Oct 20 21:32:54 2014 +0200
@@ -79,9 +79,9 @@
   order to make parsing of proof documents work properly.  Command
   keywords need to be classified according to their structural role in
   the formal text.  Examples may be seen in Isabelle/HOL sources
-  itself, such as @{keyword "keywords"}~@{verbatim "\"typedef\""}
+  itself, such as @{keyword "keywords"}~@{verbatim \<open>"typedef"\<close>}
   @{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim
-  "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations
+  \<open>"datatype"\<close>} @{text ":: thy_decl"} for theory-level declarations
   with and without proof, respectively.  Additional @{syntax tags}
   provide defaults for document preparation (\secref{sec:tags}).
 
diff -r 33be43d70147 -r e5f809f52f26 src/Doc/Isar_Ref/Symbols.thy
--- a/src/Doc/Isar_Ref/Symbols.thy	Mon Oct 20 20:43:02 2014 +0200
+++ b/src/Doc/Isar_Ref/Symbols.thy	Mon Oct 20 21:32:54 2014 +0200
@@ -6,13 +6,13 @@
 
 text \<open>
   Isabelle supports an infinite number of non-ASCII symbols, which are
-  represented in source text as @{verbatim "\\"}@{verbatim "<"}@{text
+  represented in source text as @{verbatim \<open>\\<close>}@{verbatim "<"}@{text
   name}@{verbatim ">"} (where @{text name} may be any identifier).  It
   is left to front-end tools how to present these symbols to the user.
   The collection of predefined standard symbols given below is
   available by default for Isabelle document output, due to
-  appropriate definitions of @{verbatim "\\"}@{verbatim isasym}@{text
-  name} for each @{verbatim "\\"}@{verbatim "<"}@{text name}@{verbatim
+  appropriate definitions of @{verbatim \<open>\isasym\<close>}@{text
+  name} for each @{verbatim \<open>\\<close>}@{verbatim "<"}@{text name}@{verbatim
   ">"} in the @{verbatim isabellesym.sty} file.  Most of these symbols
   are displayed properly in Isabelle/jEdit and {\LaTeX} generated from Isabelle.