aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/NewDoc.texi
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1998-11-06 15:36:10 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1998-11-06 15:36:10 +0000
commit58dac20ec5ce08ca07ab225f34e9f26f53964aa0 (patch)
tree83aa62e11f0244acdac372c795c8da80b46dbe89 /doc/NewDoc.texi
parent160e5099123f2c7d57e8503ea1f79faaf7c877fa (diff)
Added plea for help and made logo in intro only for HTML.
Diffstat (limited to 'doc/NewDoc.texi')
-rw-r--r--doc/NewDoc.texi21
1 files changed, 15 insertions, 6 deletions
diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi
index bbfd8d73..9362d6fa 100644
--- a/doc/NewDoc.texi
+++ b/doc/NewDoc.texi
@@ -39,7 +39,9 @@ END-INFO-DIR-ENTRY
@subtitle Organise your proofs with Emacs!
@subtitle Proof General @value{version}
@subtitle @value{last-update}
+@iftex
@image{ProofGeneral}
+@end iftex
@author D. Aspinall, H. Goguen, T. Kleymann and D. Sequeira
@page
@vskip 0pt plus 1filll
@@ -199,12 +201,10 @@ Obtaining and Installing Proof General
@node Introducing Proof General
@chapter Introducing Proof General
-@c maybe not in TeX, just put on title page.
-@c not in info, it can't deal with images.
-@c Maybe in HTML because it doesn't appear in titles?
-
+@c would like the logo on the title page really but
+@c it doesn't seem to work there for html.
@ifhtml
-@image{ProofGeneral}
+<IMG SRC="ProofGeneral.jpg" ALT="[ Proof General logo ]" >
@end ifhtml
@dfn{Proof General} is a generic Emacs interface for proof assistants,
@@ -221,6 +221,15 @@ cut-and-paste to reassemble the pieces. Proof General keeps track of
which proof steps have been processed by the prover, and prevents you
editing them accidently. You can undo steps as usual.
+Our aim is provide a powerful and configurable Emacs mode which helps
+user-interaction with interactive proof assistants. Please help us with
+this aim! Configure Proof General for your proof assistant, by adding
+features at the generic level wherever possible. See
+@c Stupid undefined node error her, why?
+@xref{Adding A New Proof Assistant}
+for more details, and send ideas, comments, patches,
+and code to @code{proofgen@@dcs.ed.ac.uk}.
+
@menu
* Quick start guide::
@@ -1878,7 +1887,7 @@ Fixes for some of these may be provided in a future release.
@menu
* Granularity of Atomic Command Sequences::
* Handling Multiple Files::
-* Adding A New Proof Assistant::
+* Adding A New Proof Assistant::
* Literature::
@end menu