1.1 --- a/doc-src/IsarRef/Thy/document/syntax.tex Fri May 02 22:47:58 2008 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/syntax.tex Fri May 02 22:48:51 2008 +0200
1.3 @@ -93,16 +93,16 @@
1.4 presented in \cite{isabelle-ref}.
1.5
1.6 \begin{matharray}{rcl}
1.7 - \indexdef{}{syntax}{ident}\isa{ident} & = & letter\,quasiletter^* \\
1.8 - \indexdef{}{syntax}{longident}\isa{longident} & = & ident (\verb,.,ident)^+ \\
1.9 - \indexdef{}{syntax}{symident}\isa{symident} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\
1.10 - \indexdef{}{syntax}{nat}\isa{nat} & = & digit^+ \\
1.11 - \indexdef{}{syntax}{var}\isa{var} & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
1.12 - \indexdef{}{syntax}{typefree}\isa{typefree} & = & \verb,',ident \\
1.13 - \indexdef{}{syntax}{typevar}\isa{typevar} & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
1.14 - \indexdef{}{syntax}{string}\isa{string} & = & \verb,", ~\dots~ \verb,", \\
1.15 - \indexdef{}{syntax}{altstring}\isa{altstring} & = & \backquote ~\dots~ \backquote \\
1.16 - \indexdef{}{syntax}{verbatim}\isa{verbatim} & = & \verb,{*, ~\dots~ \verb,*,\verb,}, \\[1ex]
1.17 + \indexdef{}{syntax}{ident}\mbox{\isa{ident}} & = & letter\,quasiletter^* \\
1.18 + \indexdef{}{syntax}{longident}\mbox{\isa{longident}} & = & ident (\verb,.,ident)^+ \\
1.19 + \indexdef{}{syntax}{symident}\mbox{\isa{symident}} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\
1.20 + \indexdef{}{syntax}{nat}\mbox{\isa{nat}} & = & digit^+ \\
1.21 + \indexdef{}{syntax}{var}\mbox{\isa{var}} & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
1.22 + \indexdef{}{syntax}{typefree}\mbox{\isa{typefree}} & = & \verb,',ident \\
1.23 + \indexdef{}{syntax}{typevar}\mbox{\isa{typevar}} & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
1.24 + \indexdef{}{syntax}{string}\mbox{\isa{string}} & = & \verb,", ~\dots~ \verb,", \\
1.25 + \indexdef{}{syntax}{altstring}\mbox{\isa{altstring}} & = & \backquote ~\dots~ \backquote \\
1.26 + \indexdef{}{syntax}{verbatim}\mbox{\isa{verbatim}} & = & \verb,{*, ~\dots~ \verb,*,\verb,}, \\[1ex]
1.27
1.28 letter & = & latin ~|~ \verb,\,\verb,<,latin\verb,>, ~|~ \verb,\,\verb,<,latin\,latin\verb,>, ~|~ greek ~|~ \\
1.29 & & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
1.30 @@ -123,12 +123,12 @@
1.31 & & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
1.32 \end{matharray}
1.33
1.34 - The syntax of \isa{string} admits any characters, including
1.35 + The syntax of \mbox{\isa{string}} admits any characters, including
1.36 newlines; ``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) need to be escaped by a backslash; arbitrary
1.37 character codes may be specified as ``\verb|\|\isa{ddd}'',
1.38 with three decimal digits. Alternative strings according to
1.39 - \isa{altstring} are analogous, using single back-quotes instead.
1.40 - The body of \isa{verbatim} may consist of any text not
1.41 + \mbox{\isa{altstring}} are analogous, using single back-quotes instead.
1.42 + The body of \mbox{\isa{verbatim}} may consist of any text not
1.43 containing ``\verb|*|\verb|}|''; this allows
1.44 convenient inclusion of quotes without further escapes. The greek
1.45 letters do \emph{not} include \verb|\<lambda>|, which is already used
1.46 @@ -265,8 +265,8 @@
1.47 \end{rail}
1.48
1.49 Positional instantiations are indicated by giving a sequence of
1.50 - terms, or the placeholder ``\verb|_|'' (underscore), which
1.51 - means to skip a position.
1.52 + terms, or the placeholder ``\isa{{\isacharunderscore}}'' (underscore), which means to
1.53 + skip a position.
1.54
1.55 \indexoutertoken{inst}\indexoutertoken{insts}
1.56 \begin{rail}
1.57 @@ -295,8 +295,8 @@
1.58 %
1.59 \begin{isamarkuptext}%
1.60 Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
1.61 - types and terms. Some commands such as \isa{\isacommand{types}} (see
1.62 - \secref{sec:types-pure}) admit infixes only, while \isa{\isacommand{consts}} (see \secref{sec:consts}) and \isa{\isacommand{syntax}} (see
1.63 + types and terms. Some commands such as \mbox{\isa{\isacommand{types}}} (see
1.64 + \secref{sec:types-pure}) admit infixes only, while \mbox{\isa{\isacommand{consts}}} (see \secref{sec:consts}) and \mbox{\isa{\isacommand{syntax}}} (see
1.65 \secref{sec:syn-trans}) support the full range of general mixfixes
1.66 and binders.
1.67
1.68 @@ -315,8 +315,8 @@
1.69
1.70 Here the \railtok{string} specifications refer to the actual mixfix
1.71 template (see also \cite{isabelle-ref}), which may include literal
1.72 - text, spacing, blocks, and arguments (denoted by ``\verb|_|'');
1.73 - the special symbol ``\verb|\<index>|'' (printed as ``\isa{{\isasymindex}}'')
1.74 + text, spacing, blocks, and arguments (denoted by ``\isa{{\isacharunderscore}}''); the
1.75 + special symbol ``\verb|\<index>|'' (printed as ``\isa{{\isasymindex}}'')
1.76 represents an index argument that specifies an implicit structure
1.77 reference (see also \secref{sec:locale}). Infix and binder
1.78 declarations provide common abbreviations for particular mixfix
1.79 @@ -413,9 +413,9 @@
1.80
1.81 \item selections from named facts \isa{a{\isacharparenleft}i{\isacharparenright}} or \isa{a{\isacharparenleft}j\ {\isacharminus}\ k{\isacharparenright}},
1.82
1.83 - \item literal fact propositions using \indexref{}{syntax}{altstring}\isa{altstring} syntax
1.84 + \item literal fact propositions using \indexref{}{syntax}{altstring}\mbox{\isa{altstring}} syntax
1.85 \verb|`|\isa{{\isasymphi}}\verb|`| (see also method
1.86 - \indexref{}{method}{fact}\isa{fact} in \secref{sec:pure-meth-att}).
1.87 + \indexref{}{method}{fact}\mbox{\isa{fact}} in \secref{sec:pure-meth-att}).
1.88
1.89 \end{enumerate}
1.90
1.91 @@ -429,7 +429,7 @@
1.92 internal dummy fact, which will be ignored later on. So only the
1.93 effect of the attribute on the background context will persist.
1.94 This form of in-place declarations is particularly useful with
1.95 - commands like \isa{\isacommand{declare}} and \isa{\isacommand{using}}.
1.96 + commands like \mbox{\isa{\isacommand{declare}}} and \mbox{\isa{\isacommand{using}}}.
1.97
1.98 \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
1.99 \indexouternonterm{thmdef}\indexouternonterm{thmref}
1.100 @@ -493,8 +493,8 @@
1.101 the typing refers to all variables, while in \isa{a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n} the naming refers to all propositions collectively.
1.102 Isar language elements that refer to \railnonterm{vars} or
1.103 \railnonterm{props} typically admit separate typings or namings via
1.104 - another level of iteration, with explicit \indexref{}{keyword}{and}\isa{\isakeyword{and}}
1.105 - separators; e.g.\ see \isa{\isacommand{fix}} and \isa{\isacommand{assume}} in
1.106 + another level of iteration, with explicit \indexref{}{keyword}{and}\mbox{\isa{\isakeyword{and}}}
1.107 + separators; e.g.\ see \mbox{\isa{\isacommand{fix}}} and \mbox{\isa{\isacommand{assume}}} in
1.108 \secref{sec:proof-context}.%
1.109 \end{isamarkuptext}%
1.110 \isamarkuptrue%
1.111 @@ -505,24 +505,24 @@
1.112 %
1.113 \begin{isamarkuptext}%
1.114 \begin{matharray}{rcl}
1.115 - \indexdef{}{antiquotation}{theory}\isa{theory} & : & \isarantiq \\
1.116 - \indexdef{}{antiquotation}{thm}\isa{thm} & : & \isarantiq \\
1.117 - \indexdef{}{antiquotation}{prop}\isa{prop} & : & \isarantiq \\
1.118 - \indexdef{}{antiquotation}{term}\isa{term} & : & \isarantiq \\
1.119 - \indexdef{}{antiquotation}{const}\isa{const} & : & \isarantiq \\
1.120 - \indexdef{}{antiquotation}{abbrev}\isa{abbrev} & : & \isarantiq \\
1.121 - \indexdef{}{antiquotation}{typeof}\isa{typeof} & : & \isarantiq \\
1.122 - \indexdef{}{antiquotation}{typ}\isa{typ} & : & \isarantiq \\
1.123 - \indexdef{}{antiquotation}{thm-style}\isa{thm{\isacharunderscore}style} & : & \isarantiq \\
1.124 - \indexdef{}{antiquotation}{term-style}\isa{term{\isacharunderscore}style} & : & \isarantiq \\
1.125 - \indexdef{}{antiquotation}{text}\isa{text} & : & \isarantiq \\
1.126 - \indexdef{}{antiquotation}{goals}\isa{goals} & : & \isarantiq \\
1.127 - \indexdef{}{antiquotation}{subgoals}\isa{subgoals} & : & \isarantiq \\
1.128 - \indexdef{}{antiquotation}{prf}\isa{prf} & : & \isarantiq \\
1.129 - \indexdef{}{antiquotation}{full-prf}\isa{full{\isacharunderscore}prf} & : & \isarantiq \\
1.130 - \indexdef{}{antiquotation}{ML}\isa{ML} & : & \isarantiq \\
1.131 - \indexdef{}{antiquotation}{ML-type}\isa{ML{\isacharunderscore}type} & : & \isarantiq \\
1.132 - \indexdef{}{antiquotation}{ML-struct}\isa{ML{\isacharunderscore}struct} & : & \isarantiq \\
1.133 + \indexdef{}{antiquotation}{theory}\mbox{\isa{theory}} & : & \isarantiq \\
1.134 + \indexdef{}{antiquotation}{thm}\mbox{\isa{thm}} & : & \isarantiq \\
1.135 + \indexdef{}{antiquotation}{prop}\mbox{\isa{prop}} & : & \isarantiq \\
1.136 + \indexdef{}{antiquotation}{term}\mbox{\isa{term}} & : & \isarantiq \\
1.137 + \indexdef{}{antiquotation}{const}\mbox{\isa{const}} & : & \isarantiq \\
1.138 + \indexdef{}{antiquotation}{abbrev}\mbox{\isa{abbrev}} & : & \isarantiq \\
1.139 + \indexdef{}{antiquotation}{typeof}\mbox{\isa{typeof}} & : & \isarantiq \\
1.140 + \indexdef{}{antiquotation}{typ}\mbox{\isa{typ}} & : & \isarantiq \\
1.141 + \indexdef{}{antiquotation}{thm-style}\mbox{\isa{thm{\isacharunderscore}style}} & : & \isarantiq \\
1.142 + \indexdef{}{antiquotation}{term-style}\mbox{\isa{term{\isacharunderscore}style}} & : & \isarantiq \\
1.143 + \indexdef{}{antiquotation}{text}\mbox{\isa{text}} & : & \isarantiq \\
1.144 + \indexdef{}{antiquotation}{goals}\mbox{\isa{goals}} & : & \isarantiq \\
1.145 + \indexdef{}{antiquotation}{subgoals}\mbox{\isa{subgoals}} & : & \isarantiq \\
1.146 + \indexdef{}{antiquotation}{prf}\mbox{\isa{prf}} & : & \isarantiq \\
1.147 + \indexdef{}{antiquotation}{full-prf}\mbox{\isa{full{\isacharunderscore}prf}} & : & \isarantiq \\
1.148 + \indexdef{}{antiquotation}{ML}\mbox{\isa{ML}} & : & \isarantiq \\
1.149 + \indexdef{}{antiquotation}{ML-type}\mbox{\isa{ML{\isacharunderscore}type}} & : & \isarantiq \\
1.150 + \indexdef{}{antiquotation}{ML-struct}\mbox{\isa{ML{\isacharunderscore}struct}} & : & \isarantiq \\
1.151 \end{matharray}
1.152
1.153 The text body of formal comments (see also \secref{sec:comments})
1.154 @@ -582,7 +582,7 @@
1.155 \item [\isa{{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}}] prints theorems
1.156 \isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}. Note that attribute specifications
1.157 may be included as well (see also \secref{sec:syn-att}); the
1.158 - \indexref{}{attribute}{no-vars}\isa{no{\isacharunderscore}vars} rule (see \secref{sec:misc-meth-att}) would
1.159 + \indexref{}{attribute}{no-vars}\mbox{\isa{no{\isacharunderscore}vars}} rule (see \secref{sec:misc-meth-att}) would
1.160 be particularly useful to suppress printing of schematic variables.
1.161
1.162 \item [\isa{{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}}] prints a well-typed proposition \isa{{\isasymphi}}.
1.163 @@ -629,7 +629,7 @@
1.164
1.165 \item [\isa{{\isacharat}{\isacharbraceleft}full{\isacharunderscore}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}}] is like \isa{{\isacharat}{\isacharbraceleft}prf\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}}, but displays the full proof terms,
1.166 i.e.\ also displays information omitted in the compact proof term,
1.167 - which is denoted by ``\verb|_|'' placeholders there.
1.168 + which is denoted by ``\isa{{\isacharunderscore}}'' placeholders there.
1.169
1.170 \item [\isa{{\isacharat}{\isacharbraceleft}ML\ s{\isacharbraceright}}, \isa{{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}type\ s{\isacharbraceright}}, and \isa{{\isacharat}{\isacharbraceleft}ML{\isacharunderscore}struct\ s{\isacharbraceright}}] check text \isa{s} as ML value, type, and
1.171 structure, respectively. The source is displayed verbatim.
1.172 @@ -704,7 +704,7 @@
1.173
1.174 \item[\isa{source\ {\isacharequal}\ bool}] prints the source text of the
1.175 antiquotation arguments, rather than the actual value. Note that
1.176 - this does not affect well-formedness checks of \isa{thm}, \isa{term}, etc. (only the \isa{text} antiquotation admits arbitrary output).
1.177 + this does not affect well-formedness checks of \mbox{\isa{thm}}, \mbox{\isa{term}}, etc. (only the \mbox{\isa{text}} antiquotation admits arbitrary output).
1.178
1.179 \item[\isa{goals{\isacharunderscore}limit\ {\isacharequal}\ nat}] determines the maximum number of
1.180 goals to be printed.
1.181 @@ -756,14 +756,14 @@
1.182 specifically, e.g.\ to fold proof texts, or drop parts of the text
1.183 completely.
1.184
1.185 - For example ``\isa{\isacommand{by}}~\isa{{\isacharpercent}invisible\ auto}'' would
1.186 + For example ``\mbox{\isa{\isacommand{by}}}~\isa{{\isacharpercent}invisible\ auto}'' would
1.187 cause that piece of proof to be treated as \isa{invisible} instead
1.188 of \isa{proof} (the default), which may be either show or hidden
1.189 - depending on the document setup. In contrast, ``\isa{\isacommand{by}}~\isa{{\isacharpercent}visible\ auto}'' would force this text to be shown
1.190 + depending on the document setup. In contrast, ``\mbox{\isa{\isacommand{by}}}~\isa{{\isacharpercent}visible\ auto}'' would force this text to be shown
1.191 invariably.
1.192
1.193 Explicit tag specifications within a proof apply to all subsequent
1.194 - commands of the same level of nesting. For example, ``\isa{\isacommand{proof}}~\isa{{\isacharpercent}visible\ {\isasymdots}}~\isa{\isacommand{qed}}'' would force the
1.195 + commands of the same level of nesting. For example, ``\mbox{\isa{\isacommand{proof}}}~\isa{{\isacharpercent}visible\ {\isasymdots}}~\mbox{\isa{\isacommand{qed}}}'' would force the
1.196 whole sub-proof to be typeset as \isa{visible} (unless some of its
1.197 parts are tagged differently).%
1.198 \end{isamarkuptext}%