Lines Matching defs:The
14 The \HOL{} system can be downloaded from \url{http://hol-theorem-prover.org}.
15 The naming scheme for \holn{} releases is $\langle${\it name}$\rangle$-$\langle${\it number}$\rangle$; the release described here is \holnversion.
17 \section{The {\tt hol-info} mailing list}
19 The \texttt{hol-info} mailing list serves as a forum for discussing
29 choose another name if you want; it is not important.} The contents
52 The session in the box below shows a typical distribution directory.
53 The \HOL{} distribution has been placed on a PC running Linux in the
61 continuous session. The Unix prompt for the sessions is
69 it is of minimal interest. The meta-language \ML{} is introduced in
135 The next step is to run the \texttt{build} program. This should
139 \textsf{hol.bare} and \textsf{hol.bare.noquote}. The first of these
178 The \texttt{config-override} file need only provide values for those
183 itself. The value given for the \texttt{OS} variable must be one of
186 The string \texttt{"winNT"} is used for Microsoft Windows operating systems that are at least as recent as Windows~NT.
199 The \texttt{holdir} value must be the name of the top-level directory
200 listed in the first session above. The \texttt{OS} value should be
204 The \texttt{polymllibdir} must be a path to a directory that contains the file \texttt{libpolymain.a}.
210 ``optional'' components of the system. The first gives a string