equal
deleted
inserted
replaced
55 theory T |
55 theory T |
56 imports B\(@1\) \(\ldots\) B\(@n\) |
56 imports B\(@1\) \(\ldots\) B\(@n\) |
57 begin |
57 begin |
58 {\rmfamily\textit{declarations, definitions, and proofs}} |
58 {\rmfamily\textit{declarations, definitions, and proofs}} |
59 end |
59 end |
60 \end{ttbox} |
60 \end{ttbox}\cmmdx{theory}\cmmdx{imports} |
61 where \texttt{B}$@1$ \dots\ \texttt{B}$@n$ are the names of existing |
61 where \texttt{B}$@1$ \dots\ \texttt{B}$@n$ are the names of existing |
62 theories that \texttt{T} is based on and \textit{declarations, |
62 theories that \texttt{T} is based on and \textit{declarations, |
63 definitions, and proofs} represents the newly introduced concepts |
63 definitions, and proofs} represents the newly introduced concepts |
64 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the |
64 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the |
65 direct \textbf{parent theories}\indexbold{parent theories} of~\texttt{T}\@. |
65 direct \textbf{parent theories}\indexbold{parent theories} of~\texttt{T}\@. |