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. _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
