From 33f2f008506d69fb505760128352eb7d0ec8ffed Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 30 Jun 2002 22:43:49 +0000
Subject: New files.

---
 pgkit/README | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 pgkit/README

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
+
+
+
+		
+
-- 
cgit v1.2.3