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