1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
\DOC load_path
\TYPE {load_path : string list ref}
\SYNOPSIS
Path where HOL Light tries to find files to load.
\DESCRIBE
The reference variable {load_path} gives a list of directories. When HOL loads
files with {loadt}, it will try these places in order on all non-absolute
filenames. An initial dollar sign {$} in each path is interpreted as a
reference to the current setting of {hol_dir}. To get an actual {$} character
at the start of the filename, use two dollar signs {$$}.
\FAILURE
Not applicable.
\SEEALSO
file_on_path, help_path, hol_dir, hol_expand_directory, load_on_path, loads,
loadt, needs.
\ENDDOC
|
