[isabelle] A single way to reference AFP entries

Dear list,

I have a few entries in the AFP. These did not originate in the AFP:
They were developed outside, referencing the AFP using "$AFP/Foo/Bar",
as suggested in http://www.isa-afp.org/using.shtml

But when submitting them to the AFP, I have to change that to
"../Foo/Bar". From then on, when I want to merge changes from my
working repository to the AFP and back, I have to keep changing that.

An alternative would be to develop in the AFP repository, but that
feels quite wrong.

Another alternative is to add symbolic links to the used AFP entries to
the directory above my current project. This works, but is also not
nice, as it clutters my "projects" directory.

So I wonder: Is it not possible to device a way that allows the same
theories to work inside the AFP and outside? Why is it that within the
AFP, $AFP cannot be set appropriately (to ".." if you want)?

The reason for .. mentioned above is that "it interacts correctly with
multiple AFP installations side by side". But would setting AFP=.., if
one has to work with multiple installations, not do the same?


Dr. rer. nat. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.