From 4e5653f795b68ef30a4f365cdc9a9cc596f912ba Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 3 Oct 2014 15:31:32 +0200 Subject: Removing deactivated command Show Tree. --- doc/refman/RefMan-pro.tex | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 3e72816db9..ab2fcb802b 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!!. -\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 -- cgit v1.2.3