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
649 system's overlay file. This is needed for compilation of HOL source
779 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}).
782 Such heaps can be preloaded with source code implementing special-purpose reasoning facilities, and with various necessary background theories.
796 For example, the \texttt{realheap} above might be generated with the source in Figure~\ref{fig:realheap-makefile}.
962 The commands are not really processed by \LaTeX{}: instead the source file must first be passed through the \munge{} filter.
984 \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}.
1489 of the \LaTeX{} source file \texttt{article.tex}. Holindex loads the
1502 \LaTeX{} use these files. After modifying the source file, the munger
1574 the header of your latex source file. These file use a syntax similar to
1729 which will need to be included in the \LaTeX{} source file.