[isabelle-dev] Towards the Isabelle2014 release

Lawrence Paulson lp15 at cam.ac.uk
Thu Jun 5 16:17:43 CEST 2014

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.

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.

More information about the isabelle-dev mailing list