From f1e36dc74e323fa869ff955a633ce55a62fe621f Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 16 Jul 2000 15:18:32 +0000 Subject: Modified, now white paper contains DTDs (soon) --- html/projects/pgip.html | 1 + 1 file changed, 1 insertion(+) (limited to 'html/projects/pgip.html') diff --git a/html/projects/pgip.html b/html/projects/pgip.html index 22cc654b..073edd06 100644 --- a/html/projects/pgip.html +++ b/html/projects/pgip.html @@ -4,6 +4,7 @@ PGIP is a protocol for interactive proof to be used in the next version of Proof General. It is based around the present protocol, but implemented with a standard collection of messages rather than different messages for different proof assistants. An outline of PGIP +and an experimental DTD is given in the white paper. A first implementation of PGIP will consist of (1) a filter (or modification of the output routines) for an existing proof assistant, -- cgit v1.2.3