[isabelle-dev] AFP as Isabelle component

[Florian Haftmann]

Hi all,

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.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110825/da5fcf25/attachment.asc>