[isabelle-dev] Safe approach to hypothesis substitution

Lawrence Paulson lp15 at cam.ac.uk
Wed Sep 1 15:37:00 CEST 2010

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.

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.

More information about the isabelle-dev mailing list