diff options
| -rw-r--r-- | html/doc.phtml | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/html/doc.phtml b/html/doc.phtml index d885b0bf..bd3b1abc 100644 --- a/html/doc.phtml +++ b/html/doc.phtml @@ -33,15 +33,26 @@ list</a>. <hr> <h2>References</h2> +<p> Ideas for the future of Proof General are given here: +</p> +<ul> +<li><a href="http://www.dcs.ed.ac.uk/home/da">David Aspinall</a>. + <b><i>Proof General Kit (white paper)</i></b>. + Draft version, see + <a href="http://zermelo.dcs.ed.ac.uk/home/da/drafts/#white">here</a>. +</li> +</ul> <p> A technology overview of Proof General is given here: </p> <ul> <li> <a href="http://www.dcs.ed.ac.uk/home/da">David Aspinall</a>. <a href="papers/pgoutline.ps.gz">Proof General: A Generic Tool for Proof Development</a>. - <i>Demonstration at ETAPS 2000</i>. October 1999. + <i>Tools and Algorithms for the Construction and + Analysis of Systems, Proc TACAS 2000</i>, LNCS 1785, pp 38-42. + <br> Here are some <a href="papers/pgtalk.pdf">slides</a> - for the talk. + I used for this talk and some other presentations of Proof General. </li> </ul> <p> Proof General supports Script Management as documented in: @@ -55,7 +66,7 @@ list</a>. href="ftp://babar.inria.fr/pub/croap/bertot/jsymcomp.ps">A generic approach to building user interfaces for theorem provers</a>. - <I>Journal of Symbolic Computation</I>, 25(7), pp. 161-194, February 1998. + <i>Journal of Symbolic Computation</i>, 25(7), pp. 161-194, February 1998. </li> </ul> <p> |