aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2008-07-10 19:51:02 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2008-07-10 19:51:02 +0000
commit45b81a6bcc5369b3a7dbda0d6e423b8d9016f6fb (patch)
tree3e7d20cd69e133f71e7545b7d6b73a8d3782cdff /doc
parent1eb2741f2022efb3b48c3fd19e472a3a1c638b33 (diff)
Add doc for `isabelle-chosen-logic\'
Diffstat (limited to 'doc')
-rw-r--r--doc/ProofGeneral.texi11
1 files changed, 9 insertions, 2 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index a544321a..60723013 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -127,7 +127,7 @@ END-INFO-DIR-ENTRY
@page
@vskip 0pt plus 1filll
This manual and the program Proof General are
-Copyright @copyright{} 1998-2008 Proof General team, LFCS Edinburgh.
+Copyright © 1998-2008 Proof General team, LFCS Edinburgh.
@c
@c COPYING NOTICE
@@ -3956,6 +3956,13 @@ responsible for recording any settings that are configured when you
select @code{Isabelle -> Settings -> Save Settings}. They are stored
along with the other Emacs customization settings.
+@c TEXI DOCSTRING MAGIC: isabelle-chosen-logic
+@defvar isabelle-chosen-logic
+URL of web page for Isabelle.
+@end defvar
+
+
+
@node Isabelle customizations
@section Isabelle customizations
@@ -4287,7 +4294,7 @@ Script management as used in Proof General is described in the paper:
@itemize @bullet
@item @b{[BT98]}
-Yves Bertot and Laurent Th@'ery. @i{A generic approach to building
+Yves Bertot and Laurent Théry. @i{A generic approach to building
user interfaces for theorem provers}. Journal of
Symbolic Computation, 25(7), pp. 161-194, February 1998.
@end itemize