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.sew...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
