[isabelle-dev] Safe approach to hypothesis substitution

[Lawrence Paulson]

I always intended auto to be initial rather than terminal. I'm not aware of the unsafe mode you refer to, but it may have been introduced later.
Larry

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

> Good point - I think of auto as terminal. My understanding was that auto had both a safe and unsafe mode internally, where safe exploration is clarsimp-like and seen by the user, and unsafe exploration is fastsimp-like and kept only if it solves the goal. For tactics which continue after auto, this would put it in the clarsimp/safe group. This fits with my experience in writing the supplied patch, where some subgoal_tacs which came after autos had to be adjusted slightly.