--- a/src/Doc/Isar_Ref/Symbols.thy Tue Oct 20 23:03:46 2015 +0200
+++ b/src/Doc/Isar_Ref/Symbols.thy Tue Oct 20 23:53:40 2015 +0200
@@ -6,26 +6,24 @@
text \<open>
Isabelle supports an infinite number of non-ASCII symbols, which are
- represented in source text as @{verbatim \<open>\\<close>}@{verbatim "<"}@{text
- name}@{verbatim ">"} (where @{text name} may be any identifier). It
+ represented in source text as @{verbatim \<open>\\<close>}@{verbatim "<"}\<open>name\<close>@{verbatim ">"} (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>}@{text
- name} for each @{verbatim \<open>\\<close>}@{verbatim "<"}@{text name}@{verbatim
+ 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
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 @{text "A\<^sup>\<star>"} and @{verbatim "A\<^sub>1"} for
- @{text "A\<^sub>1"}. Sub- and superscripts that span a region of text can
- be marked up with @{verbatim "\<^bsub>"}@{text "\<dots>"}@{verbatim
- "\<^esub>"} and @{verbatim "\<^bsup>"}@{text "\<dots>"}@{verbatim "\<^esup>"}
+ such as @{verbatim "A\<^sup>\<star>"} for \<open>A\<^sup>\<star>\<close> and @{verbatim "A\<^sub>1"} 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>"}
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 @{text "\<^bold>\<alpha>"}. Note that
+ @{verbatim "\<^bold>"} such as @{verbatim "\<^bold>\<alpha>"} for \<open>\<^bold>\<alpha>\<close>. Note that
@{verbatim "\<^sup>"}, @{verbatim "\<^sub>"}, @{verbatim "\<^bold>"} cannot be combined.
Further details of Isabelle document preparation are covered in