[isabelle-dev] AFP as Isabelle component
florian.haftmann at informatik.tu-muenchen.de
Thu Aug 25 23:23:25 CEST 2011
I remember that once there was a discussion how AFP theories could be
referenced in theory headers using an environment variable AFP_THEORIES
or something similar.
Maybe the afp could be turned into an optional Isabelle component, e.g.
at ~~/contrib/afp. This would be have a couple of technical advantages:
a) Canonical path for importing AFP theories, e.g ~~/contrib/afp/thys
b) Turning AFP testall into an Isabelle tool, eliminating the need for
the -t option and similar things
c) A clear association of Isabelle distribution of AFP, with facilitates
having different Isabelle repositories on the same machine
d) Standardized directory structure, which is important for the ever
more critical matter of integration.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev