David Aspinall, Christoph
Lüth and Daniel
Winterstein. A Framework for Interactive Proof. Appears in
Towards Mechanized Mathematical Assistants, Springer LNAI 4573,
pp.161–175, 2007. Download as
pdf (315k).
David Aspinall, Christoph
Lüth and Burkhart
Wolff.
Assisted Proof Document Authoring.
Appears in Mathematical Knowledge Management 2005 (MKM ‘05),
Springer LNAI 3863, p. 65–80, 2005.
Download as
pdf (307k).
David Aspinall and Christoph
Lüth.
Proof General meets IsaWin — combining text-based and graphical
user interfaces.
Long version of paper presented at UITP
‘03. Appears in
ENTCS,
Download as
pdf (344k).
David Aspinall. Proof General:
A Generic Tool for Proof Development. In
Tools and Algorithms for the Construction and Analysis of Systems,
Proc TACAS 2000, LNCS 1785.
Download as ps.gz.
Here are some slides
used for this talk and some other presentations of Proof General.
Related work and older documentation
Yves Bertot and
Laurent Théry.
A generic approach to building user interfaces for theorem
provers. In Journal of Symbolic Computation,
25(7), pp. 161-194, February 1998.
Download as ps.gz.
This paper describes Script Management, also supported by
Proof General.
Yves Bertot, Thomas
Kleymann-Schreiber and Dilip Sequeira. Implementing Proof by
Pointing without a Structure Editor. LFCS Technical Report
ECS-LFCS-97-368.
Also published as Rapport de recherche de
l’Inria Sophia Antipolis:
RR-3286.
This paper describes PG’s implementation of Proof by Pointing.