blob: a88902f54ea49de3633a2c3769399b780ea0055d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
HOL Proof General, for HOL 98.
Written by David Aspinall.
$Id$
Status: not officially supported yet
Maintainer: volunteer required
HOL version: HOL 98, tested with Taupo 2
HOL homepage: http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html
========================================
This is a "technology demonstration" of Proof General for HOL 98.
It may work with other versions of HOL, but is untested (please let me
know if you try).
It has basic script management support, with a little bit of
decoration of scripts and output.
There is support for X Symbol, but not using a proper token language.
Try writing "philosophy" !
I have written this in the hope that somebody from the HOL community
will adopt it, maintain and improve it, and thus turn it into a proper
instantiation of Proof General.
------------
Notes:
There are some problems at the moment. HOL proof scripts often use
batch-oriented single step tactic proofs, but Proof General does not
offer an easy way to edit these kind of proofs. The "Boomburg-HOL"
Emacs interface by Koichi Takahashi and Masima Hagiya addressed this,
and to some extent so perhaps does the Emacs interface supplied with
HOL. Perhaps one of these could be embedded/reimplemented inside
Proof General. Implemented in a generic way, managing batch vs
interactive proofs would also be useful for Isabelle.
Another problem is that HOL scripts sometimes use SML structures,
which can cause confusion because Proof General does not really parse
SML, it just looks for semicolons. This could be improved by taking a
better parser (e.g. from sml mode).
These improvements would be worthwhile contributions to Proof General
and also provide the HOL community with a nice front end.
Please have a go!
|
