On Fri, 14 Mar 2014, Andreas Lochbihler wrote:
IIRC, the AFP policy is (was?) that all entries that import at least one
theory from HOL-Library are based on HOL-Library.
I can't speak for the AFP editors, but that might be just some
old-fashioned custom. In general it does not even work out, since the
session images structure is just a tree, without the possibility of merge
nodes.
I have recently started to rethink the way theory imports from other
sessions are specified, which would remove any coincidence on how the
image tree was formed, oddities like "../Foo/Bar" vs just Bar, and
oddities about fluctuating options [document = false]. As usual such
reforms are encumbered by having to think thrice: for batch build, PIDE,
Proof General. Getting rid of the latter would speed the process.
I'd like to see a situation where one can just fire up the Prover IDE and
edit any of the AFP theories without thinking about accidental session
images.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
