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

Lawrence Paulson lp15 at cam.ac.uk
Mon Jan 13 23:57:01 CET 2014

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.


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.

More information about the isabelle-dev mailing list