doc-src/TutorialI/basics.tex
changeset 15358 26c501c5024d
parent 15141 a95c2ff210ba
child 15429 b08a5eaf22e3
--- a/doc-src/TutorialI/basics.tex	Thu Dec 02 00:44:54 2004 +0100
+++ b/doc-src/TutorialI/basics.tex	Thu Dec 02 10:36:20 2004 +0100
@@ -57,7 +57,7 @@
 begin
 {\rmfamily\textit{declarations, definitions, and proofs}}
 end
-\end{ttbox}
+\end{ttbox}\cmmdx{theory}\cmmdx{imports}
 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