From cd2b7bac2a48fcefb3a43b7b179aae3ff0511eca Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 24 Jan 2008 19:28:48 +0000
Subject: Add key binding for ML {* *} short cut.

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

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 9e6c405c..78d26a3e 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3779,6 +3779,8 @@ Inserts "\<^isub>"  (identifier subscript letter)
 Inserts "\<^raw:>"  (raw LaTeX text)
 @item C-c C-a C-a
 Inserts "@@@{text ""@}"  (anti-quotation).
+@item C-c C-a C-x
+Inserts "ML {* *}"  (inline ML code).
 @end table
 
 Command termination via `@code{;}' is an optional feature of Isar
-- 
cgit v1.2.3