[isabelle-dev] Towards the Isabelle2014 release

[Lawrence Paulson]

I certainly agree with your point of view, but I would immediately insert the local context around any proof that causes problems rather than waste time trying to fix it.

Maybe we could then invite the maintainers of the entries to update their proofs if they wish.
Larry

On 5 Jun 2014, at 04:44, Thomas Sewell <thomas.sewell at nicta.com.au> wrote:

> In particular, I want to avoid ever changing the setting globally. I've had some bad experiences in the past with theories with differing global configurations, which means that the location of a tactic and the include graphs of theories start having subtle effects on the way the tactics run. It's a mess.
> 
> I've started running through the AFP, and it doesn't look too bad. I'll report on this again in the next few days.