--- In dcproof@yahoogroups.com, Thomas Heye <1910-131@...> wrote:
>
> Hi,
> recently I noticed that 'delete all references' also deletes
> statements even if they don't reference the line being deleted.
(How)
> can I prevent that?
>
> I was working on a proof, and I had proven a small "lemma" I
thought
> might be useful in subsequent proofs, but later it turned out to be
> irrelevant, so I wanted to delete it. Since it wasn't used at all,
I
> thought it wasn't a problem at all. But I was warned that deleting
> this would delete 100 or so statements-- far more lines than the
proof
> of that lemma.
>

In addition to all direct references to a selected line of proof,
the Delete All References command will also delete subsequent
statements in which the usage of a variable would change (e.g. from
a "green" variable to a "red" variable) as a result of the
deletion. (Send me the proof and I will be able to be more
specific.) It is one of the pitfalls of reusing the same variable
name in different sections of your proof.

In the proof in question, I recommend leaving the lemma in your
proof and inserting a suitable comment, telling the reader to skip
the next n lines of proof. Not very elegant, I know. In future, I
recommend either (a) having separate proofs for each lemma and
inserting the lemma as a premise in subsequent proofs, or (b) being
very careful in your reuse of variables.

Regards,
Dan