1.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex	Tue Jan 08 17:32:40 2002 +0100
     1.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex	Tue Jan 08 17:43:21 2002 +0100
     1.3 @@ -174,11 +174,11 @@
     1.4    type declaration given above merely serves for syntactic purposes,
     1.5    and is not checked for consistency with the real constant.
     1.6  
     1.7 -  \medskip We may now write either \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in input, while output uses the nicer syntax of $xsymbols$,
     1.8 -  provided that print mode is active.  Such an arrangement is
     1.9 -  particularly useful for interactive development, where users may
    1.10 -  type plain ASCII text, but gain improved visual feedback from the
    1.11 -  system.
    1.12 +  \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in
    1.13 +  input, while output uses the nicer syntax of $xsymbols$, provided
    1.14 +  that print mode is active.  Such an arrangement is particularly
    1.15 +  useful for interactive development, where users may type plain ASCII
    1.16 +  text, but gain improved visual feedback from the system.
    1.17  
    1.18    \begin{warn}
    1.19    Alternative syntax declarations are apt to result in varying
    1.20 @@ -362,7 +362,7 @@
    1.21    document (\verb,\documentclass, etc.), and to include the generated
    1.22    files $T@i$\texttt{.tex} for each theory.  The generated
    1.23    \texttt{session.tex} will contain {\LaTeX} commands to include all
    1.24 -  theory output files in topologically sorted order, so
    1.25 +  generated files in topologically sorted order, so
    1.26    \verb,\input{session}, in \texttt{root.tex} does the job in most
    1.27    situations.
    1.28  
    1.29 @@ -414,9 +414,9 @@
    1.30    Further packages may be required in particular applications, e.g.\
    1.31    for unusual Isabelle symbols.
    1.32  
    1.33 -  \medskip Additional files for the {\LaTeX} stage should be included
    1.34 -  in the \texttt{MySession/document} directory, e.g.\ further {\TeX}
    1.35 -  sources or graphics.  In particular, adding \texttt{root.bib} here
    1.36 +  \medskip Additional files for the {\LaTeX} stage may be included in
    1.37 +  the directory \texttt{MySession/document}, too, such as {\TeX}
    1.38 +  sources or graphics).  In particular, adding \texttt{root.bib} here
    1.39    (with that specific name) causes an automatic run of \texttt{bibtex}
    1.40    to process a bibliographic database; see also \texttt{isatool
    1.41    document} covered in \cite{isabelle-sys}.