From b36448114c3853311e31f533657a4d4e78b2820c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 12 Jun 2017 12:38:05 +0200 Subject: Remove commented documentation for Show Tree. --- doc/refman/RefMan-pro.tex | 16 ---------------- 1 file changed, 16 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 0760d716e..b66659dc8 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -427,22 +427,6 @@ 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 Node}\comindex{Show Node}\\ -% Not yet documented - \item {\tt Show Proof.}\comindex{Show Proof}\\ It displays the proof term generated by the tactics that have been applied. -- cgit v1.2.3