| changeset 15141 | a95c2ff210ba |
| parent 15136 | 1275417e3930 |
| child 15358 | 26c501c5024d |
--- a/doc-src/TutorialI/basics.tex Wed Aug 18 11:09:40 2004 +0200 +++ b/doc-src/TutorialI/basics.tex Wed Aug 18 11:44:17 2004 +0200 @@ -53,7 +53,7 @@ format of a theory \texttt{T} is \begin{ttbox} theory T -import B\(@1\) \(\ldots\) B\(@n\) +imports B\(@1\) \(\ldots\) B\(@n\) begin {\rmfamily\textit{declarations, definitions, and proofs}} end