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

[Lawrence Paulson]

I’m impressed with your determination to slog through so many changes, but I am not sure that we have the right to impose this on our users, which is why I would prefer one of the other solutions, namely (1) contextual information if available (2) some sort of compatibility mode.

Thank you very much indeed for taking up this matter again, because I do believe it is important.

Larry

On 13 Jan 2014, at 12:38, Thomas Sewell <Thomas.Sewell at nicta.com.au> wrote:

> If there's interest in getting this change installed, I'll slog through these, and then figure out what's broken and what's expected to be broken in the latest tip of Isabelle and in the AFP. I'd call for volunteers to help with that bit though.