From d5408248f4f8ce638d313fc656b7ed3a4069129a Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Mon, 21 Jan 2013 14:13:56 +0000
Subject: - implement proof-script insertion

---
 doc/PG-adapting.texi  | 4 +++-
 doc/ProofGeneral.texi | 1 +
 2 files changed, 4 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 67248cb4..9d359bb0 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -2755,7 +2755,9 @@ is encoded in the message before the string itself.
 
 For debugging purposes Prooftree can save all input in a file.
 This feature can be turned on in the @code{Debug} tab of the
-Prooftree configuration dialog or with option @code{-tee}.
+Prooftree configuration dialog or with option @code{-tee}. The
+text that Prooftree sends to Proof General can be found in buffer
+@code{*proof-tree*}.
 
 
 @node Guards
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 30e19cfc..72ac5751 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3160,6 +3160,7 @@ given existential variable.
 your proof to try a different approach.
 @item Trigger a retract (undo) operation with a selected sequent
 as target.
+@item Insert proof scripts from the proof tree in the current buffer.
 @end itemize
 
 For a more elaborated description please consult the help dialog
-- 
cgit v1.2.3