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:4
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
This message on isabelle-users is related and suggests how to avoid the
OutOfMemory:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-April/msg00116.html
Tobias
On 06/06/2014 06:40, Thomas Sewell wrote:
> While fixing theories in the AFP, I arrived in a strange situation where
> "isabel
