diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-08-28 15:13:43 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-08-28 15:13:43 +0000 |
| commit | 287e4358c1322eda62c3c5fa2e86c0ad8a18628b (patch) | |
| tree | 1ccca8327bf863d859dfa48e4cd74e261f848c04 /doc | |
| parent | 7600f85e72f8d863b46088690cca75aa47d7ee82 (diff) | |
Updated magic
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/PG-adapting.texi | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 9443be97..10b3739a 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -308,7 +308,7 @@ directory and elisp file for the mode, which will be where @samp{PROOF-HOME-DIRECTORY} is the value of the variable @code{proof-home-directory}. -The default value is @code{((demoisa "Isabelle Demo" "\\.ML$") (isar "Isabelle/Isar" "\\.thy$") (isa "Isabelle" "\\.ML$\\|\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$") (plastic "Plastic" "\\.lf$") (hol98 "HOL" "\\.sml$") (twelf "Twelf" "\\.elf$"))}. +The default value is @code{((demoisa "Isabelle Demo" "\\.ML$") (isar "Isabelle/Isar" "\\.thy$") (isa "Isabelle" "\\.ML$\\|\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$") (hol98 "HOL" "\\.sml$") (plastic "Plastic" "\\.lf$") (twelf "Twelf" "\\.elf$"))}. @end defopt @@ -1943,7 +1943,7 @@ in the @code{proof-assistants} setting. @c TEXI DOCSTRING MAGIC: proof-assistants @defopt proof-assistants Choice of proof assistants to use with Proof General.@* -A list of symbols chosen from: @code{'demoisa} @code{'isar} @code{'isa} @code{'lego} @code{'coq} @code{'plastic} @code{'hol98} @code{'twelf}. +A list of symbols chosen from: @code{'demoisa} @code{'isar} @code{'isa} @code{'lego} @code{'coq} @code{'hol98} @code{'plastic} @code{'twelf}. Each proof assistant defines its own instance of Proof General, providing session control, script management, etc. Proof General will be started automatically for the assistants chosen here. |