[isabelle-dev] Safe approach to hypothesis substitution

Lawrence Paulson lp15 at cam.ac.uk
Wed Sep 1 15:47:02 CEST 2010


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.




More information about the isabelle-dev mailing list