[ << ] [ >> ] [Top] [Contents] [Index] [ ? ]

References

A short overview of the Proof General system is described in the note:

  • [Asp00] David Aspinall. Proof General: A Generic Tool for Proof Development. Tools and Algorithms for the Construction and Analysis of Systems, Proc TACAS 2000. LNCS 1785.

Script management as used in Proof General is described in the paper:

  • [BT98] Yves Bertot and Laurent Théry. A generic approach to building user interfaces for theorem provers. Journal of Symbolic Computation, 25(7), pp. 161-194, February 1998.

Proof General has support for proof by pointing, as described in the document:

  • [BKS97] 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
[ << ] [ >> ] [Top] [Contents] [Index] [ ? ]

This document was generated on November 21, 2024 using texi2html 1.82.