1.1 --- a/doc-src/IsarRef/Thy/document/syntax.tex	Mon Apr 28 14:41:32 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/syntax.tex	Mon Apr 28 14:42:13 2008 +0200
     1.3 @@ -294,8 +294,8 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
     1.7 -  types and terms.  Some commands such as \isa{types} (see
     1.8 -  \S\ref{sec:types-pure}) admit infixes only, while \isa{consts} (see \S\ref{sec:consts}) and \isa{syntax} (see
     1.9 +  types and terms.  Some commands such as \isa{\isacommand{types}} (see
    1.10 +  \S\ref{sec:types-pure}) admit infixes only, while \isa{\isacommand{consts}} (see \S\ref{sec:consts}) and \isa{\isacommand{syntax}} (see
    1.11    \S\ref{sec:syn-trans}) support the full range of general mixfixes
    1.12    and binders.
    1.13  
    1.14 @@ -426,7 +426,7 @@
    1.15    involving an internal dummy fact, which will be ignored later on.
    1.16    So only the effect of the attribute on the background context will
    1.17    persist.  This form of in-place declarations is particularly useful
    1.18 -  with commands like \isa{declare} and \isa{using}.
    1.19 +  with commands like \isa{\isacommand{declare}} and \isa{\isacommand{using}}.
    1.20  
    1.21    \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
    1.22    \indexouternonterm{thmdef}\indexouternonterm{thmref}
    1.23 @@ -490,8 +490,8 @@
    1.24    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.25    Isar language elements that refer to \railnonterm{vars} or
    1.26    \railnonterm{props} typically admit separate typings or namings via
    1.27 -  another level of iteration, with explicit \indexref{}{keyword}{and}\isa{and}
    1.28 -  separators; e.g.\ see \isa{fix} and \isa{assume} in
    1.29 +  another level of iteration, with explicit \indexref{}{keyword}{and}\isa{\isakeyword{and}}
    1.30 +  separators; e.g.\ see \isa{\isacommand{fix}} and \isa{\isacommand{assume}} in
    1.31    \S\ref{sec:proof-context}.%
    1.32  \end{isamarkuptext}%
    1.33  \isamarkuptrue%
    1.34 @@ -751,14 +751,14 @@
    1.35    specifically, e.g.\ to fold proof texts, or drop parts of the text
    1.36    completely.
    1.37  
    1.38 -  For example ``\isa{by}~\isa{{\isacharpercent}invisible\ auto}'' would
    1.39 +  For example ``\isa{\isacommand{by}}~\isa{{\isacharpercent}invisible\ auto}'' would
    1.40    cause that piece of proof to be treated as \isa{invisible} instead
    1.41    of \isa{proof} (the default), which may be either show or hidden
    1.42 -  depending on the document setup.  In contrast, ``\isa{by}~\isa{{\isacharpercent}visible\ auto}'' would force this text to be shown
    1.43 +  depending on the document setup.  In contrast, ``\isa{\isacommand{by}}~\isa{{\isacharpercent}visible\ auto}'' would force this text to be shown
    1.44    invariably.
    1.45  
    1.46    Explicit tag specifications within a proof apply to all subsequent
    1.47 -  commands of the same level of nesting.  For example, ``\isa{proof}~\isa{{\isacharpercent}visible\ {\isasymdots}}~\isa{qed}'' would force the
    1.48 +  commands of the same level of nesting.  For example, ``\isa{\isacommand{proof}}~\isa{{\isacharpercent}visible\ {\isasymdots}}~\isa{\isacommand{qed}}'' would force the
    1.49    whole sub-proof to be typeset as \isa{visible} (unless some of its
    1.50    parts are tagged differently).%
    1.51  \end{isamarkuptext}%