From 6631e485b86747bac15a85cd83e0c62d824ce8ce Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 20 Jun 2018 16:16:28 +0200 Subject: Add a good reference for Proof-General as suggested by Clément. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- doc/sphinx/biblio.bib | 15 +++++++++++++++ doc/sphinx/introduction.rst | 2 +- 2 files changed, 16 insertions(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index bb881da04..bfa96621f 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -3,6 +3,21 @@ @String{lnai = "Lecture Notes in Artificial Intelligence"} @String{SV = "{Sprin-ger-Verlag}"} +@InCollection{Asp00, + Title = {Proof General: A Generic Tool for Proof Development}, + Author = {Aspinall, David}, + Booktitle = {Tools and Algorithms for the Construction and + Analysis of Systems, {TACAS} 2000}, + Publisher = {Springer Berlin Heidelberg}, + Year = {2000}, + Editor = {Graf, Susanne and Schwartzbach, Michael}, + Pages = {38--43}, + Series = {Lecture Notes in Computer Science}, + Volume = {1785}, + Doi = {10.1007/3-540-46419-0_3}, + ISBN = {978-3-540-67282-1}, +} + @Book{Bar81, author = {H.P. Barendregt}, publisher = {North-Holland}, diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 5a628f4ea..73da5e802 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -34,7 +34,7 @@ are processed from a file. step, and query the system for available theorems and definitions. The interactive mode is generally run with the help of an IDE, such as CoqIDE, documented in :ref:`coqintegrateddevelopmentenvironment`, - Emacs with Proof-General (available at https://proofgeneral.github.io/), + Emacs with Proof-General :cite:`Asp00` (available at https://proofgeneral.github.io/), or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq). The `coqtop` read-eval-print-loop can also be used directly, for debugging purposes. -- cgit v1.2.3