Add FAQ about favourites

1 files changed, 19 insertions, 4 deletions

diff --git a/FAQ b/FAQ
index 946ddb47..a687fb09 100644
--- a/FAQ
+++ b/FAQ
@@ -275,12 +275,18 @@ A. There are X-Symbol fonts at sizes of 12, 14, 18 and 24.  The standard size
 
 -----------------------------------------------------------------
 
+Q. The "Favourites" feature to insert/send fixed strings is great, 
+   but I'd like to define a command which takes arguments.
 
-Q. I see spurious ^M characters at the end of lines in the 
-   windows showing output from the prover.  How can I remove
-   them?
+A. You can do that in Elisp with a command like this: 
+
+    (proof-definvisible isar-theorem
+      '(format "thm %s" (read-string "theorem: "))
+       [(control t)])
+
+   (NB: it binds the key C-c C-a C-t).  See the documentation for
+   `proof-definvisible' and `proof-defshortcut`.
 
-A. Customize the value of `proof-shell-strip-crs-from-output'.
 
 -----------------------------------------------------------------
 
@@ -293,6 +299,15 @@ A. Your Emacs session has loaded a version of xml.el from somewhere other
 
 -----------------------------------------------------------------
 
+Q. I see spurious ^M characters at the end of lines in the 
+   windows showing output from the prover.  How can I remove
+   them?
+
+A. Customize the value of `proof-shell-strip-crs-from-output'.
+
+-----------------------------------------------------------------
+
+
 Q. Can I join any mailing lists for Proof General?
 
 A. Of course, email "proofgeneral-request@informatics.ed.ac.uk"