diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-06-30 22:43:49 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-06-30 22:43:49 +0000 |
| commit | 33f2f008506d69fb505760128352eb7d0ec8ffed (patch) | |
| tree | 9e2d00522cf930eebda63e2ee8bd1ec404cb9b4d /pgkit | |
| parent | edc0c638c41b8ee8b03f1d5eeba881fc8fb7e35d (diff) | |
New files.
Diffstat (limited to 'pgkit')
| -rw-r--r-- | pgkit/README | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/pgkit/README b/pgkit/README new file mode 100644 index 00000000..81e6ad00 --- /dev/null +++ b/pgkit/README @@ -0,0 +1,20 @@ +About Proof General Kit +======================= + +Proof General has been Emacs based so far, but plans are afoot to +liberate it from the points and parentheses of Emacs Lisp. The +successor framework, Proof General Kit, proposes that proof assistants +use a *standard* XML-based protocol for interactive proof, dubbed +PGIP. + +PGIP will allow a middleware layer for many interactive proof tools +and interface components (including Emacs). The design of PGIP was +made possible by the present Emacs-based Proof General framework. + +For more on Proof General Kit, see +http://www.proofgeneral.org/kit.html + + + + + |