[isabelle] THY path



Hi!

is there a way of telling Isabelle where to search for THY files? From the error message in PG-Emacs when trying to load a non-existing THY file, I get that the standard search is "." and "$ISABELLE_HOME/src/HOL/Library". I would like to extend this list.

The reason is that we have 3 entries in the AFP which our development is based on (currently we have local copies of the corresponding THY files). To me, it would seem as an overkill, if I had to incrementally construct heap images for
1) HOL-First-Entry
2) HOL-First-and-Second-Entry
3) HOL-First-and-Second-and-Third-Entry
and then use 'HOL-First-and-Second-and-Third-Entry instead' of 'HOL'.

What do you think? How do other users that base their work on AFP entries, handle such situations? Andreas? ;)

cheers

chris





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