aboutsummaryrefslogtreecommitdiff
path: root/generic
diff options
context:
space:
mode:
authorDavid Aspinall1998-11-03 14:40:24 +0000
committerDavid Aspinall1998-11-03 14:40:24 +0000
commitaaaeaeb988028e4445a91ac60c2700ddbdf577b2 (patch)
treef02b102cafc11276f300978a7cf30c4d8d1f81ea /generic
parentea353681e654246b993c868e691eba991e7584a9 (diff)
Improved docstrings
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-config.el6
1 files changed, 4 insertions, 2 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 3c90d5e9..02f2a02b 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -361,12 +361,14 @@ The script buffer's comment-end is set to this string plus a space."
:group 'prover-config)
(defcustom proof-save-with-hole-regexp nil
- "Matches a named save command"
+ "Regexp which matches a command to save a named theorem.
+Match number 2 should be the name of the theorem saved."
:type 'regexp
:group 'proof-script)
(defcustom proof-goal-with-hole-regexp nil
- "Matches a saved goal command"
+ "Regexp which matches a command used to issue and name a goal.
+Match number 2 should be the name of the goal issued."
:type 'regexp
:group 'proof-script)