[isabelle-dev] Safe approach to hypothesis substitution mark II
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