50 \textbf{theory} is a named collection of types, functions, and theorems, |
50 \textbf{theory} is a named collection of types, functions, and theorems, |
51 much like a module in a programming language or a specification in a |
51 much like a module in a programming language or a specification in a |
52 specification language. In fact, theories in HOL can be either. The general |
52 specification language. In fact, theories in HOL can be either. The general |
53 format of a theory \texttt{T} is |
53 format of a theory \texttt{T} is |
54 \begin{ttbox} |
54 \begin{ttbox} |
55 theory T = B\(@1\) + \(\cdots\) + B\(@n\): |
55 theory T |
|
56 import B\(@1\) \(\ldots\) B\(@n\) |
|
57 begin |
56 {\rmfamily\textit{declarations, definitions, and proofs}} |
58 {\rmfamily\textit{declarations, definitions, and proofs}} |
57 end |
59 end |
58 \end{ttbox} |
60 \end{ttbox} |
59 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 |
60 theories that \texttt{T} is based on and \textit{declarations, |
62 theories that \texttt{T} is based on and \textit{declarations, |
61 definitions, and proofs} represents the newly introduced concepts |
63 definitions, and proofs} represents the newly introduced concepts |
62 (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 |
63 direct \textbf{parent theories}\indexbold{parent theories} of~\texttt{T}\@. |
65 direct \textbf{parent theories}\indexbold{parent theories} of~\texttt{T}\@. |
64 Everything defined in the parent theories (and their parents, recursively) is |
66 Everything defined in the parent theories (and their parents, recursively) is |