diff options
| author | Christophe Raffalli | 2000-11-13 10:30:57 +0000 |
|---|---|---|
| committer | Christophe Raffalli | 2000-11-13 10:30:57 +0000 |
| commit | b1f847966dc77d5b1c84ba779c95fdada5055073 (patch) | |
| tree | ebc2e23c8a1eeb3d6c53d2f6ba1a18496cfd3943 /doc | |
| parent | bebf19e9d69866a9f403700282e213e69877d721 (diff) | |
*** empty log message ***
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 2e5ce9d0..7bd11e91 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -369,7 +369,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$") (af2 "Af2" "\\.af2$") (hol98 "HOL" "\\.sml$") (plastic "Plastic" "\\.lf$") (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$") (af2 "Af2" "\\.af2$") (hol98 "HOL" "\\.sml$") (acl2 "ACL2" "\\.acl2$") (plastic "Plastic" "\\.lf$") (twelf "Twelf" "\\.elf$"))}. @end defopt @@ -2445,7 +2445,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{'af2} @code{'hol98} @code{'plastic} @code{'twelf}. +A list of symbols chosen from: @code{'demoisa} @code{'isar} @code{'isa} @code{'lego} @code{'coq} @code{'af2} @code{'hol98} @code{'acl2} @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. |