aboutsummaryrefslogtreecommitdiffhomepage
path: root/html/doc.phtml
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-05-16 08:26:34 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-05-16 08:26:34 +0000
commite5f81135e0f864bc7552fd9bf5b8c8423c2d6232 (patch)
tree9be9cd24a9daf09d5235723747881033389777f5 /html/doc.phtml
parent43271266a4b7ffc1f6849910541b85078b68d825 (diff)
Better reference to TACAS paper. Added link to white paper draft.
Diffstat (limited to 'html/doc.phtml')
-rw-r--r--html/doc.phtml17
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>