diff -r 760e21900b01 -r 28e788ca2c5d src/Doc/Isar_Ref/Symbols.thy
--- a/src/Doc/Isar_Ref/Symbols.thy	Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Isar_Ref/Symbols.thy	Thu Oct 22 21:16:49 2015 +0200
@@ -6,25 +6,24 @@
 
 text \<open>
   Isabelle supports an infinite number of non-ASCII symbols, which are
-  represented in source text as @{verbatim \<open>\\<close>}@{verbatim "<"}\<open>name\<close>@{verbatim ">"} (where \<open>name\<close> may be any identifier).  It
+  represented in source text as \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> (where \<open>name\<close> 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 \<open>\isasym\<close>}\<open>name\<close> for each @{verbatim \<open>\\<close>}@{verbatim "<"}\<open>name\<close>@{verbatim
-  ">"} in the @{verbatim isabellesym.sty} file.  Most of these symbols
+  appropriate definitions of \<^verbatim>\<open>\isasym\<close>\<open>name\<close> for each \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> in
+  the \<^verbatim>\<open>isabellesym.sty\<close> file.  Most of these symbols
   are displayed properly in Isabelle/jEdit and {\LaTeX} generated from Isabelle.
 
   Moreover, any single symbol (or ASCII character) may be prefixed by
-  @{verbatim "\<^sup>"} for superscript and @{verbatim "\<^sub>"} for subscript,
-  such as @{verbatim "A\<^sup>\<star>"} for \<open>A\<^sup>\<star>\<close> and @{verbatim "A\<^sub>1"} for
+  \<^verbatim>\<open>\<^sup>\<close> for superscript and \<^verbatim>\<open>\<^sub>\<close> for subscript,
+  such as \<^verbatim>\<open>A\<^sup>\<star>\<close> for \<open>A\<^sup>\<star>\<close> and \<^verbatim>\<open>A\<^sub>1\<close> for
   \<open>A\<^sub>1\<close>.  Sub- and superscripts that span a region of text can
-  be marked up with @{verbatim "\<^bsub>"}\<open>\<dots>\<close>@{verbatim
-  "\<^esub>"} and @{verbatim "\<^bsup>"}\<open>\<dots>\<close>@{verbatim "\<^esup>"}
+  be marked up with \<^verbatim>\<open>\<^bsub>\<close>\<open>\<dots>\<close>\<^verbatim>\<open>\<^esub>\<close> and \<^verbatim>\<open>\<^bsup>\<close>\<open>\<dots>\<close>\<^verbatim>\<open>\<^esup>\<close>
   respectively, but note that there are limitations in the typographic
   rendering quality of this form.  Furthermore, all ASCII characters
   and most other symbols may be printed in bold by prefixing
-  @{verbatim "\<^bold>"} such as @{verbatim "\<^bold>\<alpha>"} for \<open>\<^bold>\<alpha>\<close>.  Note that
-  @{verbatim "\<^sup>"}, @{verbatim "\<^sub>"}, @{verbatim "\<^bold>"} cannot be combined.
+  \<^verbatim>\<open>\<^bold>\<close> such as \<^verbatim>\<open>\<^bold>\<alpha>\<close> for \<open>\<^bold>\<alpha>\<close>.  Note that
+  \<^verbatim>\<open>\<^sup>\<close>, \<^verbatim>\<open>\<^sub>\<close>, \<^verbatim>\<open>\<^bold>\<close> cannot be combined.
 
   Further details of Isabelle document preparation are covered in
   \chref{ch:document-prep}.