diff options
author | Christophe Raffalli <christophe.raffalli@univ-savoie.fr> | 2000-11-10 17:58:16 +0000 |
---|---|---|
committer | Christophe Raffalli <christophe.raffalli@univ-savoie.fr> | 2000-11-10 17:58:16 +0000 |
commit | bebf19e9d69866a9f403700282e213e69877d721 (patch) | |
tree | b6e1bca7d5d5c4d6a81b510aebbe455cfd52089d /doc | |
parent | a33a0182a3115bb1591c9f5874635c621e7d190e (diff) |
*** empty log message ***
Diffstat (limited to 'doc')
-rw-r--r-- | doc/PG-adapting.texi | 14 | ||||
-rw-r--r-- | doc/docstring-magic.el | 3 |
2 files changed, 9 insertions, 8 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 057d4ad7..2e5ce9d0 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -108,7 +108,7 @@ END-INFO-DIR-ENTRY @c so we take it out for now. @c Ideally would like some way of generating eps from @c the .jpg file. -@image{ProofGeneralPortrait} +@c image{ProofGeneralPortrait} @end ifset @end iftex @author David Aspinall with T. Kleymann @@ -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$") (acl2 "ACL2" "\\.acl2$") (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$") (plastic "Plastic" "\\.lf$") (twelf "Twelf" "\\.elf$"))}. @end defopt @@ -828,7 +828,9 @@ for @samp{@code{proof-script-next-entity-regexps}} used for function menus. @c TEXI DOCSTRING MAGIC: proof-goal-with-hole-regexp @defvar proof-goal-with-hole-regexp Regexp which matches a command used to issue and name a goal.@* -Match number 2 should be the name of the goal issued. +The name of the theorem is build from the variable +@code{proof-goal-with-hole-result} using the same convention as +@code{query-replace-regexp}. Used for setting names of goal..save regions and for default @code{function-menu} configuration in @code{proof-script-find-next-entity}. @@ -854,7 +856,9 @@ Matches a save command. @c TEXI DOCSTRING MAGIC: proof-save-with-hole-regexp @defvar proof-save-with-hole-regexp Regexp which matches a command to save a named theorem.@* -Match number 2 should be the name of the theorem saved. +The name of the theorem is build from the variable +@code{proof-save-with-hole-result} using the same convention as +@code{query-replace-regexp}. Used for setting names of goal..save regions and for default @code{function-menu} configuration in @code{proof-script-find-next-entity}. @@ -2441,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{'acl2} @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{'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. diff --git a/doc/docstring-magic.el b/doc/docstring-magic.el index 7673ee89..5550f324 100644 --- a/doc/docstring-magic.el +++ b/doc/docstring-magic.el @@ -15,9 +15,6 @@ (require 'proof-compat) (require 'proof-utils) - -(provide 'sym-lock) ; Hack for af2: sym-lock gives error when loaded, why? - ;; FIXME: Loading several prover files at once is a bit of a problem ;; with new config mechanism. ;; Could abstract more code in proof-site.el to avoid duplication here. |