Software Engineering Documentation

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.

====== Hypatheon Document Viewer ======

  * 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

{{:pvs:hypatheon.png?600|}}

===== Running Hypatheon in PVS =====

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.

Software Engineering Documentation

User Tools

Site Tools

Page Tools