Note that this change would affect auto, force, fast, etc. Possibly a “legacy” version of auto would help with compatibility, or otherwise some sort of option setting to (locally) restore the old behaviour in all affected methods.
Larry On 13 Jan 2014, at 15:47, Makarius <makar...@sketis.net> wrote: > With an easy escape, i.e. the alternate name of the proof method and a > confifuration option to recover the old behaviour, users should manage to > convert their old stuff reasonably well. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
