blob: 817bf469f6b2f03e379af5085de5a7fb6a397b28 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
.\" DO NOT MODIFY THIS FILE! It was generated by help2man 1.29.
.\" Well, actually, it was edited after that by me, so the dire
.\" warning should not be greatly feared.
.\" This is based on the output of: help2man ../bin/proofgeneral
.\"
.\" $Id$
.\"
.TH PROOFGENERAL "1" "March 2004" "proofgeneral" "User Commands"
.SH NAME
proofgeneral \- manual page for proofgeneral
.SH SYNOPSIS
.B proofgeneral
[\fIOPTION\fR] [\fIFILE\fR]...
.SH DESCRIPTION
Launches Emacs Proof General, editing the proof script FILE.
.SH OPTIONS
.TP
\fB\-\-emacs\fR
startup Proof General with emacs (GNU Emacs)
.TP
\fB\-\-xemacs\fR
startup Proof General with xemacs (XEmacs)
.TP
\fB\-\-emacsbin\fR <EMACS>
startup Proof General with emacs binary <EMACS>
.TP
\fB\-h\fR, \fB\-\-help\fR
show this help and exit
.TP
\fB\-v\fR, \fB\-\-version\fR
output version information and exit
.SH EXAMPLES
.TP
proofgeneral Example.thy
Load Proof General editing Isar file Example.thy
.TP
proofgeneral example.v
Load Proof General editing Coq file Example.v
.PP
For documentation and latest versions, visit http://proofgeneral.inf.ed.ac.uk.
.SH AUTHOR
David Aspinall.
.SH "REPORTING BUGS"
Report bugs to <da+pg-bugs@inf.ed.ac.uk>.
.SH COPYRIGHT
Copyright \(co 1998-2004 LFCS, University of Edinburgh, UK.
.br
This is free software; see the source for copying conditions.
.SH "SEE ALSO"
The full documentation for Proof General is available within
the program, and also as the Texinfo manual. This should be
available by the command
.IP
.B info ProofGeneral
.PP
if the info file has been installed. There is a second
manual containing instructions on adapting Proof General
to new proof assistants:
.IP
.B info PG-adapting
.PP
Ordinary users do not need to consult this manual.
|
