• At the command line, type “hypatheon”.
• The user interface below appears.
• Select “Theory” in the type.
• Browse for a keyword, e.g. “reals” or “real_props” for real number axioms and lemmas

Starting Hypatheon from PVS (to run it in PVS-client mode) requires a simple bootstrapping process. To support this process, the file '.hypatheon-emacs' will be copied by quick_install to the user's home directory. Then the following two lines will be appended to your .pvsemacs file:

(load-file "~/.hypatheon-emacs")
;(start-hypatheon-client)    ;; uncomment for automatic starting

Within a PVS instance that was started using the .pvsemacs lines above, issue M-x start-hypatheon-client to bring up the GUI. Alternatively, if the function call (start-hypatheon-client) appears uncommented in your .pvsemacs file, Hypatheon will be launched automatically during the PVS startup phase.