blob: 34c32e32716f3e8e7210f85517203e6f9d90de4f (
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
|
HOL Light in Proof General.
Written by David Aspinall.
Status: not officially supported yet
Maintainer: volunteer required
HOL-Light version:
HOL homepage: http://hol.sourceforge.net
========================================
This is a "technology demonstration" of Proof General for HOL-Light.
I have written this in the hope that somebody from the HOL-Light
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 might also be useful for other provers.
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!
$Id$
|
