From eff936289abc4d7ca2cf29c33b1b1ecb8094e7e3 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 22 Sep 2005 07:57:31 +0000
Subject: Addition from Tjark Weber for new commands

---
 doc/ProofGeneral.texi | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index dcd3f1d9..144525f7 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3839,8 +3839,12 @@ by white space as usual in Isar.
 
 @node Specific commands for Isabelle/Isar
 @subsection Specific commands for Isabelle/Isar
+@kindex C-c C-a r
+@kindex C-c C-a C-q
+@kindex C-c C-a C-d
 @kindex C-c C-a h A
 @kindex C-c C-a h C
+@kindex C-c C-a h I
 @kindex C-c C-a h S
 @kindex C-c C-a h T
 @kindex C-c C-a h a
@@ -3857,10 +3861,19 @@ help key bindings; these functions are offered within the prover help
 menu as well.
 
 @table @kbd
+@item C-c C-a r
+Invokes @code{refute} on the current subgoal.  Only available in HOL
+and derived logics.
+@item C-c C-a C-q
+Invokes @code{quickcheck} on the current subgoal.
+@item C-c C-a C-d
+Displays a draft document of the current theory.
 @item C-c C-a h A
 Shows available antiquotation commands and options.
 @item C-c C-a h C
 Shows the current Classical Reasoner context.
+@item C-c C-a h I
+Shows the current set of induct/cases rules.
 @item C-c C-a h S
 Shows the current Simplifier context.
 @item C-c C-a h T
-- 
cgit v1.2.3