On 05.06.2014 05:44, Thomas Sewell 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
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
While fixing theories in the AFP, I arrived in a strange situation where
isabelle build -D thys would no longer find and check the remaining
unbuilt theories.
Instead, I got a java OutOfMemory exception on the java heap. This is
before anything starts building - I take it java has run out of
