The reference variable help_path gives a list of directories. When using the
online help function, HOL Light will search in these places for help files.
An initial dollar sign $ in each path is interpreted as a reference to the
current setting of hol_dir. To get an actual $ at the start of the
filename, actually use two dollar signs $$.