1.1 --- a/doc-src/TutorialI/basics.tex	Mon Aug 16 19:06:59 2004 +0200
     1.2 +++ b/doc-src/TutorialI/basics.tex	Mon Aug 16 19:47:01 2004 +0200
     1.3 @@ -52,11 +52,13 @@
     1.4  specification language. In fact, theories in HOL can be either. The general
     1.5  format of a theory \texttt{T} is
     1.6  \begin{ttbox}
     1.7 -theory T = B\(@1\) + \(\cdots\) + B\(@n\):
     1.8 +theory T
     1.9 +import B\(@1\) \(\ldots\) B\(@n\)
    1.10 +begin
    1.11  {\rmfamily\textit{declarations, definitions, and proofs}}
    1.12  end
    1.13  \end{ttbox}
    1.14 -where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
    1.15 +where \texttt{B}$@1$ \dots\ \texttt{B}$@n$ are the names of existing
    1.16  theories that \texttt{T} is based on and \textit{declarations,
    1.17      definitions, and proofs} represents the newly introduced concepts
    1.18  (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the