1PROOFGENERAL(1)                  User Commands                 PROOFGENERAL(1)
2
3
4

NAME

6       proofgeneral - manual page for proofgeneral ()
7

SYNOPSIS

9       proofgeneral [OPTION] [FILE]...
10

DESCRIPTION

12       Launches Emacs Proof General, editing the proof script FILE.
13

OPTIONS

15       --emacs
16              startup Proof General with emacs (GNU Emacs)
17
18       --xemacs
19              startup Proof General with xemacs (XEmacs)
20
21       --emacsbin <EMACS>
22              startup Proof General with emacs binary <EMACS>
23
24       -h, --help
25              show this help and exit
26
27       -v, --version
28              output version information and exit
29
30       Unrecognized options are passed to Emacs, along with file names.
31

EXAMPLES

33       proofgeneral Example.thy
34              Load Proof General editing Isar file Example.thy
35
36       proofgeneral example.v
37              Load Proof General editing Coq file Example.v
38
39       For   documentation   and   latest   versions,  visit  http://proofgen
40       eral.inf.ed.ac.uk.
41

REPORTING BUGS

43       Report bugs to <da+pg-bugs@inf.ed.ac.uk>.
44
45       David Aspinall.
46
48       Copyright © 1998-2005 LFCS, University of Edinburgh, UK.
49       This is free software; see the source for copying conditions.
50

SEE ALSO

52       The full documentation for proofgeneral is maintained as a Texinfo man‐
53       ual.   If  the info and proofgeneral programs are properly installed at
54       your site, the command
55
56              info proofgeneral
57
58       should give you access to the complete manual.
59
60
61
62proofgeneral ()                   August 2005                  PROOFGENERAL(1)
Impressum