[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

# 11. HOL Proof General

HOL Proof General is a "technology demonstration" of Proof General for HOL4 (aka HOL98). This means that only a basic instantiation has been provided, and that it is not yet supported as a maintained instantiation of Proof General.

HOL Proof General has basic script management support, with a little bit of decoration of scripts and output. It does not rely on a modified version of HOL, so the pattern matching may be fragile in certain cases. Support for multiple files deduces dependencies automatically, so there is no interaction with the HOL make system yet.

See the ‘`example.sml`’ file for a demonstration proof script which works with Proof General.

Note that HOL proof scripts often use batch-oriented single step tactic proofs, but Proof General does not (yet) offer an easy way to edit these kind of proofs. They will replay simply as a single step proof and you will need to convert from the interactive to batch form as usual if you wish to obtain batch proofs. Also note that Proof General does not contain an SML parser, so there can be problems if you write complex ML in proof scripts.

HOL Proof General may work with variants of HOL other than HOL98, but is untested. Probably a few of the settings would need to be changed in a simple way, to cope with small differences in output between the systems. (Please let us know if you modify the HOL98 version for another variant of HOL).

Perhaps somebody from the HOL community is willing to adopt HOL Proof General and support and improve it. Please volunteer!

[ << ] | [ >> ] |  |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

This document was generated by David Aspinall on July, 24 2008 using texi2html 1.78.