1.1 --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 22:00:39 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 22:01:30 2008 +0100
     1.3 @@ -135,31 +135,45 @@
     1.4    \end{supertabular}
     1.5    \end{center}
     1.6  
     1.7 -  The syntax of @{syntax string} admits any characters, including
     1.8 +  A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown,
     1.9 +  which is internally a pair of base name and index (ML type @{ML_type
    1.10 +  indexname}).  These components are either separated by a dot as in
    1.11 +  @{text "?x.1"} or @{text "?x7.3"} or run together as in @{text
    1.12 +  "?x1"}.  The latter form is possible if the base name does not end
    1.13 +  with digits.  If the index is 0, it may be dropped altogether:
    1.14 +  @{text "?x"} and @{text "?x0"} and @{text "?x.0"} all refer to the
    1.15 +  same unknown, with basename @{text "x"} and index 0.
    1.16 +
    1.17 +  The syntax of @{syntax_ref string} admits any characters, including
    1.18    newlines; ``@{verbatim "\""}'' (double-quote) and ``@{verbatim
    1.19    "\\"}'' (backslash) need to be escaped by a backslash; arbitrary
    1.20    character codes may be specified as ``@{verbatim "\\"}@{text ddd}'',
    1.21    with three decimal digits.  Alternative strings according to
    1.22 -  @{syntax altstring} are analogous, using single back-quotes instead.
    1.23 -  The body of @{syntax verbatim} may consist of any text not
    1.24 +  @{syntax_ref altstring} are analogous, using single back-quotes
    1.25 +  instead.
    1.26 +
    1.27 +  The body of @{syntax_ref verbatim} may consist of any text not
    1.28    containing ``@{verbatim "*"}@{verbatim "}"}''; this allows
    1.29 -  convenient inclusion of quotes without further escapes.  The greek
    1.30 -  letters do \emph{not} include @{verbatim "\<lambda>"}, which is already used
    1.31 -  differently in the meta-logic.
    1.32 +  convenient inclusion of quotes without further escapes.  There is no
    1.33 +  way to escape ``@{verbatim "*"}@{verbatim "}"}''.  If the quoted
    1.34 +  text is {\LaTeX} source, one may usually add some blank or comment
    1.35 +  to avoid the critical character sequence.
    1.36 +
    1.37 +  Source comments take the form @{verbatim "(*"}~@{text
    1.38 +  "\<dots>"}~@{verbatim "*)"} and may be nested, although the user-interface
    1.39 +  might prevent this.  Note that this form indicates source comments
    1.40 +  only, which are stripped after lexical analysis of the input.  The
    1.41 +  Isar syntax also provides proper \emph{document comments} that are
    1.42 +  considered as part of the text (see \secref{sec:comments}).
    1.43  
    1.44    Common mathematical symbols such as @{text \<forall>} are represented in
    1.45    Isabelle as @{verbatim \<forall>}.  There are infinitely many Isabelle
    1.46    symbols like this, although proper presentation is left to front-end
    1.47    tools such as {\LaTeX} or Proof~General with the X-Symbol package.
    1.48    A list of standard Isabelle symbols that work well with these tools
    1.49 -  is given in \cite[appendix~A]{isabelle-sys}.
    1.50 -  
    1.51 -  Source comments take the form @{verbatim "(*"}~@{text
    1.52 -  "\<dots>"}~@{verbatim "*)"} and may be nested, although the user-interface
    1.53 -  might prevent this.  Note that this form indicates source comments
    1.54 -  only, which are stripped after lexical analysis of the input.  The
    1.55 -  Isar syntax also provides proper \emph{document comments} that are
    1.56 -  considered as part of the text (see \secref{sec:comments}).
    1.57 +  is given in \cite[appendix~A]{isabelle-sys}.  Note that @{verbatim
    1.58 +  "\<lambda>"} does not belong to the @{text letter} category, since it is
    1.59 +  already used differently in the Pure term language.
    1.60  *}
    1.61  
    1.62