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 $$.