Lines Matching refs:source
45 \HOL{} source, one can get a listing of the entrypoints found in the
65 \verb+help "Tactic"+ & \HOL{} source structure information \\
107 source directory. A single invocation of \holmake{} will compute
587 system's overlay file. This is needed for compilation of HOL source
714 In Moscow~ML, \texttt{hol} starts up by visibly (and relatively slowly) ``loading'' the various source files that provide the system's functionality (\eg, \ml{bossLib}).
717 Such heaps can be preloaded with source code implementing special-purpose reasoning facilities, and with various necessary background theories.
731 For example, the \texttt{realheap} above might be generated with the source in Figure~\ref{fig:realheap-makefile}.
893 The commands are not really processed by \LaTeX{}: instead the source file must first be passed through the \munge{} filter.
915 \paragraph{Before Starting} In order to use the munger, one must ``include'' (use the \texttt{\bs{}usepackage} command) the \texttt{holtexbasic.sty} style-file, which is found in the HOL source directory \texttt{src/TeX}.
1306 of the \LaTeX{} source file \texttt{article.tex}. Holindex loads the
1319 \LaTeX{} use these files. After modifying the source file, the munger
1391 the header of your latex source file. These file use a syntax similar to
1545 which will need to be included in the \LaTeX{} source file.