1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
\DOC hol_dir
\TYPE {hol_dir : string ref}
\SYNOPSIS
Base directory in which HOL Light is installed.
\DESCRIBE
This reference variable holds the directory (folder) for the base of the HOL
Light distribution. This information is used, for example, when loading files
with {loads}. Normally set to the current directory when HOL Light is loaded or
built, but picked up from the system variable {HOLLIGHT_DIR} if it is defined.
\FAILURE
Not applicable.
\EXAMPLE
On my laptop, the value is:
{
# !hol_dir;;
val it : string = "/home/johnh/holl"
}
\USES
Ensuring that HOL Light can find any libraries or other system files needed to
support proofs.
\SEEALSO
load_path, loads.
\ENDDOC
|
