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/ProofGeneral.texi | 1 + 1 file changed, 1 insertion(+) (limited to 'doc/ProofGeneral.texi') 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