[isabelle-dev] Safe approach to hypothesis substitution

[Lawrence Paulson]

This sounds logical. But what about auto? Like the other three, it is used to perform obvious steps in a proof, and it is not terminal.
Larry

On 1 Sep 2010, at 14:17, Thomas Sewell wrote:

> Let me try to explain the difference from the perspective of a user. There are three classical tools that will behave differently: safe, clarify and clarsimp. Each of these will, when it would have substituted and removed equalities in the past, now substitute those equalities, possibly reorient them, and leave them as hypotheses.