From 59671e6efc4992445fe8ce4e05f70470828b3d64 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 6 Oct 1999 10:44:39 +0000
Subject: proof-try-command is deprecated

---
 doc/ProofGeneral.texi | 17 -----------------
 1 file changed, 17 deletions(-)

(limited to 'doc')

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 2b005810..d140173f 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1128,8 +1128,6 @@ from a proof script.  Here are the keybindings and functions.
 @code{proof-help}
 @item C-c C-c
 @code{proof-interrupt-process}
-@item C-c t
-@code{proof-try-command}
 @item C-c C-v
 @code{proof-execute-minibuffer-cmd}
 @item C-c C-f
@@ -1167,21 +1165,6 @@ Issues a command based on @var{arg} to the assistant, using @code{proof-find-the
 The user is prompted for an argument.
 @end deffn
 
-
-@c TEXI DOCSTRING MAGIC: proof-try-command
-@deffn Command proof-try-command &optional unclosed-comment-fun
-Process the command at point, but don't add it to the locked region. 
-
-Supplied to let the user to test the types and values of
-expressions. Checks via the function @code{proof-state-preserving-p} that the
-command won't change the proof state, but this isn't guaranteed to be
-foolproof and may cause Proof General to lose sync with the prover.
-
-Default action if inside a comment is just to go until the start of
-the comment. If you want something different, put it inside
-@var{unclosed-comment-fun}.
-@end deffn
-
 @c TEXI DOCSTRING MAGIC: proof-execute-minibuffer-cmd
 @deffn Command proof-execute-minibuffer-cmd 
 Prompt for a command in the minibuffer and send it to proof assistant.@*
-- 
cgit v1.2.3