diff -r f00857c7539b -r 1275417e3930 doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Mon Aug 16 19:06:59 2004 +0200
+++ b/doc-src/TutorialI/basics.tex	Mon Aug 16 19:47:01 2004 +0200
@@ -52,11 +52,13 @@
 specification language. In fact, theories in HOL can be either. The general
 format of a theory \texttt{T} is
 \begin{ttbox}
-theory T = B\(@1\) + \(\cdots\) + B\(@n\):
+theory T
+import B\(@1\) \(\ldots\) B\(@n\)
+begin
 {\rmfamily\textit{declarations, definitions, and proofs}}
 end
 \end{ttbox}
-where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
+where \texttt{B}$@1$ \dots\ \texttt{B}$@n$ are the names of existing
 theories that \texttt{T} is based on and \textit{declarations,
     definitions, and proofs} represents the newly introduced concepts
 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the