From f9eed8fe55720eaac6177447cee990aab1afaa18 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 29 May 2000 15:53:00 +0000
Subject: Updated with new keybindings for Coq, Lego.

---
 doc/ProofGeneral.texi | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

(limited to 'doc')

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index da2d7091..abddac3d 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2982,11 +2982,11 @@ common commands:
 @kindex C-c I 
 @kindex C-c R 
 @table @kbd
-@item C-c a i   
+@item C-c C-a C-i   
 intros
-@item C-c a I   
+@item C-c C-a C-I   
 Intros
-@item C-c a R   
+@item C-c C-a C-R   
 Refine
 @end table
 
@@ -3051,14 +3051,16 @@ but does not have integrated file management or proof-by-pointing yet.
 
 Coq Proof General supplies the following key-bindings:
 @table @kbd
-@item C-c a i   
+@item C-c C-a C-i   
 Inserts ``Intros '' 
-@item C-c a a
+@item C-c C-a C-a
 Inserts ``Apply '' 
-@item C-c a s
+@item C-c C-a C-s
 Inserts ``Section ''
-@item C-c a e
+@item C-c C-a C-e
 Inserts ``End <section-name>.'' (this should work well with nested sections).
+@item C-c C-a C-o
+Prompts for a SearchIsos argument.
 @end table
 
 @node Editing multiple proofs
-- 
cgit v1.2.3