Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
load_on_path : string list -> string -> unit
SYNOPSIS
Finds a file on a path and loads it into HOL Light.
DESCRIPTION
When given a filename and a path, the file is found either directly by its
filename or on the given path, as explained in file_on_path. 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 $$.) It is then loaded into HOL, updating the
list of loaded files.
FAILURE CONDITIONS
Fails if the file is not found or generates an exception when loaded (e.g. a
syntax problem or runtime exception).