Removing deactivated command Show Tree.

1 files changed, 12 insertions, 12 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 3e72816db..ab2fcb802 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -328,18 +328,18 @@ This command displays the current goals.
   This tactics script may contain some holes (subgoals not yet proved).
   They are printed under the form \verb!<Your Tactic Text here>!.
 
-\item {\tt Show Tree.}\comindex{Show Tree}\\
-This command can be seen as a more structured way of
-displaying the state of the proof than that 
-provided by {\tt Show Script}. Instead of just giving
-the list of tactics that have been applied, it 
-shows the derivation tree constructed by then. 
-Each node of the tree contains the conclusion
-of the corresponding sub-derivation (i.e. a
-goal with its corresponding local context) and 
-the tactic that has generated all the 
-sub-derivations. The leaves of this tree are
-the goals which still remain to be proved.
+%% \item {\tt Show Tree.}\comindex{Show Tree}\\
+%% This command can be seen as a more structured way of
+%% displaying the state of the proof than that 
+%% provided by {\tt Show Script}. Instead of just giving
+%% the list of tactics that have been applied, it 
+%% shows the derivation tree constructed by then. 
+%% Each node of the tree contains the conclusion
+%% of the corresponding sub-derivation (i.e. a
+%% goal with its corresponding local context) and 
+%% the tactic that has generated all the 
+%% sub-derivations. The leaves of this tree are
+%% the goals which still remain to be proved.
 
 %\item {\tt Show Node}\comindex{Show Node}\\
 %        Not yet documented