--- 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
--- 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>
--- 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
--- 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}).
--- 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.