aboutsummaryrefslogtreecommitdiffhomepage
path: root/twelf/README
blob: 2d91f558d3a9220abb3ce4648e6c37c3583c8224 (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
Twelf Proof General, for Twelf.

Written by David Aspinall.

Status:	        not officially supported yet
Maintainer:     volunteer required
Twelf version:  Twelf 1.2 (and later, I hope)
Twelf homepage: http://www.twelf.org

========================================


This is a "technology demonstration" of Proof General for Twelf.

It has basic script management support, with some support for
decoration taken from the present Twelf Emacs mode.

There is support for X Symbol, but not using a proper token language,
and it seems fairly broken because Twelf's syntax highlighting
doesn't work properly with font lock.

I have written this in the hope that somebody from the Twelf community
will adopt it, maintain and improve it, and thus turn it into a proper
instantiation of Proof General.

$Id$