1PROOFGENERAL(1) User Commands PROOFGENERAL(1)
2
3
4
6 proofgeneral - manual page for proofgeneral ()
7
9 proofgeneral [OPTION] [FILE]...
10
12 Launches Emacs Proof General, editing the proof script FILE.
13
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
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
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
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)