temp_path : string ref
Directory in which to create temporary files.
Some HOL Light derived rules in the libraries (none in the core system) need to create temporary files. This is the directory in which they do so.
On my laptop:
# !temp_path;; val it : string = "/tmp"