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

Lawrence Paulson lp15 at cam.ac.uk
Mon Jan 13 15:39:55 CET 2014

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.


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.

More information about the isabelle-dev mailing list