[isabelle-dev] Safe approach to hypothesis substitution mark II

[Lawrence Paulson]

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 <makarius at 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.